Re: [Hol-info] About the experimental kernel

On 11/04/18 18:45, michael.norr...@data61.csiro.au wrote: > Could be done in principle, but I think the implementation (in particular, of > composition of substitutions) will likely be messy. I see. I will attempt it sometime. For the moment it will go as an entry in my personal to do list for

Re: [Hol-info] About the experimental kernel

Term.lazy_beta_conv, which is in turn called by Thm.Beta and Thm.Specialize. Michael On 12/4/18, 09:50, "Jeremy Dawson" wrote: On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote: > for explicit lazy beta > conversions (with an internal

Re: [Hol-info] About the experimental kernel

On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote: for explicit lazy beta conversions (with an internal explicit substitution calculus) I assume this refers to Clos, mk_clos etc in src/0/Term.sml My questions is: is this actually used? I can't see where anything in the source code

Re: [Hol-info] About the experimental kernel

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

Re: [Hol-info] About the experimental kernel

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

[Hol-info] About the experimental kernel

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