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.

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.