From: John Munroe <munddr@gmail.com>
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
From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Mar 28 2024 at 20:16 UTC