Re: [isabelle] Datatype + cardinality + polymorphismus?

Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website

Larry Paulson

> On 27 Jun 2015, at 12:06, Roger H. <s57076 at> wrote:
> Hello,
> 1. If i have datatype color = red | blue
> how do i write smth like 
> -"is c in color"...meaning "is c an instance of color?"
> -"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
> -length function..number of elements in the datatype .. so that it returns here length (color) = 2
> 2. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
> f :: color -> ??red |-> {1,2}blue |-> {True}
> cause range f = UNIV isnt right.
> Many thanks! 		 	   		  

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