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?

Hello Alfio,

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:

http://isabelle.in.tum.de/documentation.html

Inl and Inr are used in lots of places in the example theories that
come with the distribution; just use grep.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.