[opentheory-users] deductAntisym and eqMp

Ramana Kumar 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.
> Regards,
> Rob.
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131205/2416d66b/attachment.html>

More information about the opentheory-users mailing list