Re: [isabelle] Defining Union Types



Thank you all for the quick replies!

Cheers

On Tue, Jul 26, 2011 at 4:04 AM, Christian Sternagel <
christian.sternagel at uibk.ac.at> wrote:

> Talking of the sum type... I think it would be good to have it more easily
> accessible. Currently, e.g., I have to write "Sum_Type.Projr" to get the
> right projection. As far as I can see it is mainly for internal use of some
> packages. But something like Haskell's Either would be useful for the
> library (together with a bunch of useful functions and lemmas).
>
> cheers
>
> chris
>
>
> On 07/26/2011 07:42 AM, Tobias Nipkow wrote:
>
>> It is written "+" and defined in theory Sum_Type, which is part of Main.
>> It is hardly advertised because in most cases it is nicer to define your
>> own special datatype.
>>
>> Tobias
>>
>> Am 26/07/2011 03:57, schrieb Alfio Martini:
>>
>>> Dear Isabelle Users,
>>>
>>> Do we have in Isabelle something like a union (sum) type constructor with
>>> the corresponding injections?
>>> I went through the tutorial and did not  find use or reference to it. If
>>> there is, can anyone point to an application
>>> or a written example of  this?
>>>
>>> I assume there must be a simple way to do it.
>>>
>>> Many thanks!
>>>
>>>
>>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil




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