[opentheory-users] arguments to eqMp

[Ramana Kumar]

There may be another bug in the documentation (or implementation) to
do with eqMp.
I believe bool.art from bool-1.0 tries to do an eqMp on theorems with
these conclusions:
x = x
(T ⇔ (x = x)) ⇔ (x = x)
but the second theorem is the reflection of what you would expect
given the documentation.
On Mon, Jan 10, 2011 at 12:17 AM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> Documentation bug - now fixed. Good catch.
>
> Cheers,
>
> Joe
>
> On Sun, Jan 9, 2011 at 1:12 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Is the documentation of the file format here
>> http://www.gilith.com/research/opentheory/article.html#eqMpCommand
>> correct?
>> My reader appears to be saying that the article file corresponding to
>> bool-1.0 wants |- phi to be popped before |- phi' = psi
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>