[opentheory-users] deductAntisym and eqMp
ramana at member.fsf.org
Thu Dec 5 14:33:44 UTC 2013
I believe they are intended to be interpreted modulo alpha-convertibility,
(There's also a note at the top of the article specification saying Thm
objects are interchangeable if terms in them are alpha-convertible.)
HOL4 also uses sets-up-to-alpha for the assumptions on a sequent.
On Thu, Dec 5, 2013 at 2:18 PM, Rob Arthan <rda at lemma-one.com> wrote:
> The specifications of deductAntisym and eqMp use set operations on the
> assumptions. Are these intended to be interpreted modulo
> alpha-convertibility? (ProofPower and HOL Light both treat the assumptions
> as ordered sets using alpha-convertibility as the equality test when
> inserting and deleting elements, but I don't know about HOL4.) If the
> answer is no, then a reader for ProofPower or HOL Light is going to have to
> use some fairly horrid tricks.
> opentheory-users mailing list
> opentheory-users at gilith.com
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users