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.

Attachment: signature.asc
Description: OpenPGP digital signature

Check out the vibrant tech community on one of the world's most
engaging tech sites,!
hol-info mailing list

Reply via email to