Re: [isabelle] Defining Union Types
On Mon, Jul 25, 2011 at 6:57 PM, Alfio Martini <alfio.martini at acm.org> wrote:
> 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?
Yes, there is a sum type 'a + 'b, which has constructors Inl :: 'a =>
'a + 'b and Inr :: 'b => 'a + 'b.
I am a bit surprised that this type is mentioned nowhere in the
tutorial. However it is documented in "What's in Main", which is found
on the Isabelle documentation page:
Inl and Inr are used in lots of places in the example theories that
come with the distribution; just use grep.
This archive was generated by a fusion of
Pipermail (Mailman edition) and