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

Reply via email to