Beginning of Section Eq
L2Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
End of Section Eq
Notation. We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq.
Primitive. The name
In is a term of type
set → set → prop.
Notation. We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In. Furthermore, we may write
∀ x ∈ A, B to mean
∀ x : set, x ∈ A → B.
Primitive. The name
Empty is a term of type
set.
Primitive. The name
ordsucc is a term of type
set → set.
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc.
Primitive. The name
If_i is a term of type
prop → set → set → set.
Notation.
if cond then T else E is notation corresponding to
If_i type cond T E where
type is the inferred type of
T.
Primitive. The name
SNoLt is a term of type
set → set → prop.
Primitive. The name
SNoLe is a term of type
set → set → prop.
Primitive. The name
minus_SNo is a term of type
set → set.
Primitive. The name
add_SNo is a term of type
set → set → set.
Primitive. The name
mul_SNo is a term of type
set → set → set.
Primitive. The name
int is a term of type
set.