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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and