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
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)
"Some (1, a) :: (nat * 'a) option"
Note the lower cases in Some and None.
Defined in src/HOL/Datatype.thy
> thanks in advance.
> Tim Newsham
This archive was generated by a fusion of
Pipermail (Mailman edition) and