In HOL4 you can use the “ASSUME” primitive inference rule, passing the same term as it appears in the hypotheses (up to α-conversion). Make sure that the types of the constants are the same, for otherwise this will fail (it will be either detected and an exception is raised or a theorem is produced where the assumption was not eliminated).
On 16/08/18 11:07, Dylan Melville wrote: > Is there anyway to reference a specific assumption of the current goal as a > theorem? > ------------------------------------------------------------------------------ > 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
