[opentheory-users] Scalable LCF-style proof translation
joe at gilith.com
Fri Jul 26 22:07:05 UTC 2013
> For example, in OpenTheory if you use the const command twice on the same
> name, and then constTerm with the same type on the two resulting consts, the
> two resulting terms will not be alpha equivalent.
The two resulting terms should indeed be alpha-equivalent, and if you
have seen otherwise please report it as a bug. I made a little example
article (appended) that shows this.
# Tiny example to check that two constructed constant terms
# are alpha-equivalent - Joe Leslie-Hurd
# First construction of constant term `c : bool`
# Second construction of constant term `c : bool`
# This thm would fail if the two terms were not alpha-equivalent
More information about the opentheory-users