WhoCites
Definitions
int
2
Sections
StandardLIB
Doc
Who Cites absval?
absval
Def
|i| == if 0
i
i else -i fi
Thm*
x:
. |x|
int_nzero
Def
== {i:
| i
0 }
Thm*
Type
le_int
Def
i
j ==
j <
i
Thm*
i,j:
. i
j
nequal
Def
a
b
T ==
a = b
T
Thm*
A:Type, x,y:A. x
y
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