Terms in Isabelle are essentially terms of the (polymorphic) typed lambda calculus. When we declare a constant like:

conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35)

We are introducing a new constant called conj that has type bool ⇒ bool ⇒ bool — that is, a function that takes two values of type bool and produces another bool. The infixr annotation on the right hand side lets us use familiar notation A ∧ B instead of writing conj A B, but the meaning of A ∧ B is identical to conj A B.

AsideCurrying

• December 2, 2025
• Liam O'Connor

Functions of multiple parameters in Isabelle are typically curried, meaning that a function of type bool ⇒ bool ⇒ bool is actually a function of type bool ⇒ (bool ⇒ bool) — a function that, given a bool value, produces a function of type bool ⇒ bool.