WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites div
floor?
div_floor
Def a
n == if 0
a
a
n ;((-a) rem n)=
0
-((-a)
n) else -((-a)
n)+-1 fi
Thm*
a:
, n:
. (a
n)
eq_int
Def
i=
j == if i=j
true
; false
fi
Thm*
i,j:
. (i=
j)
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:
a
n
has structure:
div_floor(a; n)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc