[opentheory-users] Scalable LCF-style proof translation

[Joe Leslie-Hurd]

Hi Ramana,

> 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.

Cheers,

Joe

_____________________________________

# Tiny example to check that two constructed constant terms
# are alpha-equivalent - Joe Leslie-Hurd
nil
# First construction of constant term `c : bool`
"c"
const
"bool"
typeOp
nil
opType
constTerm
axiom
nil
# Second construction of constant term `c : bool`
"c"
const
"bool"
typeOp
nil
opType
constTerm
# This thm would fail if the two terms were not alpha-equivalent
thm