WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites imax?
imax
Def imax(a;b) == if a
b
b else a fi
Thm*
a,b:
. imax(a;b)
le_int
Def
i
j ==
j <
i
Thm*
i,j:
. (i
j)
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
Syntax:
imax(a;b)
has structure:
imax(a; b)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc