Thanks. An additional question: Is there some reason that prevents the experimental kernel does not have explicit substitutions, or is it just because they have not been implemented, but could be done in principle?
On 11/04/18 14:23, Konrad Slind wrote: > End users should see no difference, but occasionally a proof script > generated on top of one kernel won't run on the other. That is due to > differences in how renaming is implemented in each kernel. > > For some specific cases, one kernel performs better than the other. > The "standard" kernel runs the EVAL conversions faster, while the > experimental kernel deals better with manipulations of terms with > deeply nested binders. > > Konrad. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
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
