Re: [isabelle] Defining Union Types

On Mon, Jul 25, 2011 at 6:57 PM, Alfio Martini <alfio.martini at> 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:

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.