Re: [isabelle] more beginner questions
On Mon, Sep 24, 2007 at 05:33:51PM -1000, 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 there is (it is called char). To use them you
have to include letters in double single quotes.
E.g., the character A would be written as ''A''
> 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.
The syntax would be
datatype 'a option = None | Some 'a
But this type is already predefined... so just use the construcotrs
None and Some (taking one argument).
> 3) Do any isabelle users hang out on some real-time chat network where
> a beginner like me could pester them? For example irc.freenode.net
> #isabelle would be nice. *hint* *hint*
> I'm there, but I'm afraid I'm in no position to answer questions :)
I do not know about that.
> thanks in advance.
> Tim Newsham
This archive was generated by a fusion of
Pipermail (Mailman edition) and