[opentheory-users] opentheory tool implementing eqMp incorrectly

[Ramana Kumar]

I think there's an argument order problem. It's hard keeping track of
which argument is which though :)

The article file format says, roughly,
a :: a = b :: stack --[eqMp]--> b :: stack

Now in the opentheory tool source code,
...
      | Command.EqMp =>
        let
          val (stack,objA,objB) = ObjectStack.pop2 stack

          val obj = ObjectProv.mkEqMp {savable = savable} objA objB
...

fun pop2 stack =
...
      | obj1 :: obj0 :: objs =>
...
        in
          (stack,obj0,obj1)
        end
...

fun mkEqMp {savable} objA objB =
...
          in
            Object.Thm (Thm.eqMp a b)
          end
...

fun eqMp th1 th2 =
...
      val (c2',concl) = Term.destEq c1

      val () =
          if Term.alphaEqual c2 c2' then ()
          else raise Error "Thm.eqMp: not alpha equivalent"
...

(c2 is the conclusion of th2, c1 of th1)
But I think th2 will be the equality (a=b), not th1.