http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101&rep=rep1&type=pdf
http://www.gilith.com/talks/tphols2001-subtypes.pdf - Umair On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk <fr...@cs.ru.nl> wrote: > 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 >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
