Re: [isabelle] Defining Union Types



Before we define a new type we should rather make the existing one more
usable. But what is really needed? Haskell does not offer Projl/r at all
but lefts, rights and paritionEithers.

Tobias

Am 26/07/2011 09:03, schrieb Christian Sternagel:
> 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!
>>>
>>





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