Re: [isabelle] Product types?



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.

Larry Paulson


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.
> 
> John
> 






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