This is eta conversion. It is handled in HOL4 by the simplifier and both HOL4 and HOL Light have conversions called “ETA_CONV” that are more low level.
On 06/07/18 12:01, Dylan Melville wrote: > Is there a tactical that shows that a term is equal to the same term with an > added abstraction, for example: > > |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n > > Or even more simply > > |- f:(num->bool) <=> (\x:num. f:(num->bool) ) > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
