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
>    characters.
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
> http://www.thenewsh.com/~newsham/
> 
cheers

christian





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