On Tuesday 18 Sep 2012 20:37, Jon Lockhart wrote:
> So I have run into an error again while working on my
> specification. This time it is with the second axiomatic
> definition, the one right after Roger helped me with
> last time. Using what he had done, and from the integer
> example in the tutorial notes, I set up the evidence for
> how I thought the system would want it to be given to
> it. Unfortunately this throws an exception and I can't
> seem to massage it to be what it wants.
The first is that you use "=" in the binding display but
ProofPower requires "=^" (equal with hat on it).
You also missed the prime off the last name in the signature.
Once these are fixed rewrite solves the goal.
Proofpower mailing list