Re: [isabelle] more beginner questions



On Tuesday 25 September 2007 05:33, Tim Newsham wrote:
> 1) Is there a datatype for characters in isabelle?  I would like
>     to prove stuff about a real world grammar for a language of
>     characters.
>
Yes.  I'm not sure how you enter a single character, but you have
"''A'' :: char list" for example, and also 
 "''ABC'' :: char list" (ie two single forward quotes before and after).
Defined in src/HOL/List.thy

> 2) This is really basic but giving me a headache.  How can I make
>     an optional tuple?  I tried "('a, 'a) option"  but that didnt seem
>     to work properly.

Your  "('a, 'a)" is Haskell-style for expressing a tuple type.
Isabelle-style (and ML style) is ('a * 'a)
Thus eg 
 "Some (1, a) :: (nat * 'a) option"
Note the lower cases in Some and None.
Defined in src/HOL/Datatype.thy
>
Jeremy

> thanks in advance.
>
> Tim Newsham
> http://www.thenewsh.com/~newsham/






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