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