Hello everyone, suppose I want to evaluate the definition
let factorial = define `(fact (0) = 1) /\ (fact (SUC n) = SUC n * fact (n))`;; in the term `fact 10` in HOL-Light. Do I need to use Conversions to do this or is there a simpler way like Coq's "Eval compute" or HOL4's "EVAL"? As a context, I have constructed a function that computes a boolean result by structural recursion in HOL-Light that can be used as a certificate checker for a static analysis. The problem is that currently the certificate checking is very slow since I am using only rewrite conversions. Best regards, Heiko ------------------------------------------------------------------------------ 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
