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.

Two problems.
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

Reply via email to