Thank you! > On Jul 6, 2018, at 1:04 PM, Mario Xerxes Castelán Castro > <marioxcc...@yandex.com> wrote: > > 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 >> > > ------------------------------------------------------------------------------ > 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
------------------------------------------------------------------------------ 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
