Hi Ramana, >I think this is exactly what is impossible to do in HOL: >it is a logic of total functions.
I think that in PVS you _can_ do something like that, right? Using the predicate subtypes. Even though PVS _also_ only has total functions. And I _think_ there was a paper once about how to mimic predicate subtypes in HOL. Does anyone remember the reference? Freek _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
