WhoCites
Definitions
int
2
Sections
StandardLIB
Doc
Who Cites imax?
imax
Def
imax(a;b) == if a
b
b else a fi
Thm*
a,b:
. imax(a;b)
imin
Def
imin(a;b) == if a
b
a else b fi
Thm*
a,b:
. imin(a;b)
nat
Def
== {i:
| 0
i }
Thm*
Type
le_int
Def
i
j ==
j <
i
Thm*
i,j:
. i
j
le
Def
A
B ==
B < A
Thm*
i,j:
. i
j
Prop
lt_int
Def
i <
j == if i < j
true
; false
fi
Thm*
i,j:
. i <
j
bnot
Def
b == if b
false
else true
fi
Thm*
b:
.
b
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
About:
WhoCites
Definitions
int
2
Sections
StandardLIB
Doc