Re: [isabelle] Product types?
- To: John Munroe <munddr at gmail.com>
- Subject: Re: [isabelle] Product types?
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Mon, 3 Sep 2012 10:47:46 +0100
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <CAP0k5J4ABitQp3-27aZe5KV-0=ncHJTG6LxjOw7LAZwmrYaQyQ@mail.gmail.com>
- References: <CAP0k5J4ABitQp3-27aZe5KV-0=ncHJTG6LxjOw7LAZwmrYaQyQ@mail.gmail.com>
Ordered pairs are represented by functions.
The pair (a,b) is represented by the function "(\<lambda>x y. x = a \<and> y = b)".
Details in the file HOL/Product_Type.thy.
On 31 Aug 2012, at 16:18, John Munroe wrote:
> Hi all,
> AFAIK, Isabelle's lambda calculus is simply typed, because the types
> are built up from base types by means of =>. However, there are
> product types in HOL, so how are they encoded?
> Thanks for your time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and