Re: [isabelle] Defining Union Types
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