Thanks guys for the help. Those were a couple of little errors that I overlooked.
Regards, Jon On Tue, Sep 18, 2012 at 4:06 PM, Rob Arthan <[email protected]> wrote: > Jon, > > On 18 Sep 2012, at 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. > > > > Attached is the spec and a document containing the error. > > > > In ProofPower-Z syntax, when you write down binding, you need to use the > equals with a hat (or a double equals sign) between the signature variables > and their values (as you did when you supplied the witness to an > existential goal in an earlier proof). Also you forgot the prime on the > bound variable name numOfButtons'. If you fix that and apply rewrite_tac > your goal will be proved. > > Regards, > > Rob. > >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
