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. On Wed, Apr 11, 2018 at 10:59 AM, Mario Xerxes Castelán Castro <marioxcc...@yandex.com> wrote: > Hello. > > What are the reasons for choosing either the standard or the > experimental kernel over the other one? > > I understand that at the level of implementation, the standard kernel > uses de Bruijn indices and has support for explicit lazy beta > conversions (with an internal explicit substitution calculus) while the > experimental kernel has no lazy beta conversions and uses the same > representation for free and bound variables. But what are the > differences at the end user level? > > -- > Do not eat animals; respect them as you respect people. > https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan > > > ------------------------------------------------------------------------------ > 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
