[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Enumeration types*From*: Malcolm Dowse <dowsem@tcd.ie>*Date*: Thu, 22 Mar 2001 21:58:09 +0000*Sender*: pvs-help-owner@csl.sri.com

Hello, I have what I hope is a simple problem. In my theory, I have defined an enumeration type UType as follows: UType: TYPE = {emptyT, zeroT, succT} Now, when proving theoreoms, I am finding that in a great number of sub-goals, the prover is stating me the problem in the following form: ........ |-------- [1] emptyT?(x) [2] zeroT?(x) .. when, in fact, what I believe it really means, is as follows: [-1] succT?(x) |-------- ........ To turn the first into the second, am using the command (CASE "x = succT") which splits it into 2 subgoals, one of which is trivially proven. Is there any way of defining the type so this problem will not occur? Thanking you in advance, Malcolm Dowse

- Prev by Date:
**Model-Checking** - Next by Date:
**Re: Enumeration types** - Prev by thread:
**Re: Record-type equality bug??** - Next by thread:
**Re: Enumeration types** - Index(es):