WhoCites
Definitions
mb
structures
Sections
GenAutomata
Doc
Who Cites le
int?
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:
i
j
has structure:
le_int(i; j)
About:
WhoCites
Definitions
mb
structures
Sections
GenAutomata
Doc