Re: [isabelle] Defining Union Types

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!

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