Re: [isabelle] making use of star

>Hi James,
>the relation you want is truly relational, you cannot compute one argument
>the other. 


exactly. My point was that my bad explanation in the first place probably
led to a belief that computing states was what was required. 

I realised this morning that I'd have to provide my own ``universe'' of all
instances of states in order for such calculations to work. 

With type nat you get all the natural numbers to work with. With my type
State you get the type definition and nothing else.

Many thanks for all the help. I'll move on to lists now, thankfully!

Kind regards,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.