Jon, 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. Roger _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
