Re: [isabelle] Defining Union Types
Thank you all for the quick replies!
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).
> 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.
>> 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