Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Product types?


view this post on Zulip Email Gateway (Aug 19 2022 at 08:27):

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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:51):

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