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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to