[opentheory-users] arguments to eqMp

[Ramana Kumar]

I think it's an implementation (or package) bug, because the same
article file also tries to do eqMp on these:
T ⇔ T
(T ⇔ T) ⇔ (((λx. x) = (λx. x)) ⇔ T)

On Mon, Jan 10, 2011 at 3:55 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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
>>
>