Signature symbols in this unit

Symbol	Specification	Kind	Type
. % .	int-div	pf	Int × Int → Int with λ i, j. j ≠ 0
. % .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. * .	int-mult	f	Int × Int → Int
. * .	nat-mult	f	Nat × Nat → Nat
. + .	int-basic2	f	Int × Int → Int
. + .	nat-basic	f	Nat × Nat → Nat
. +1	int-basic1	f	Int → Int
. +1	nat-basic	f	Nat → Nat
. - .	int-abs	f	Int × Int → Int
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	int-basic1	f	Int → Int
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. / .	int-div	pf	Int × Int → Int with λ i, j. j ≠ 0
. / .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. < .	int-basic1	p	Int × Int
. < .	nat-basic	p	Nat × Nat
. > .	int-abs	p	Int × Int
. > .	nat	p	Nat × Nat
. ≤ .	int-abs	p	Int × Int
. ≤ .	nat	p	Nat × Nat
. ≥ .	int-abs	p	Int × Int
. ≥ .	nat	p	Nat × Nat
~ .	int-abs	f	Int → Int
Int	int-basic1	s
Nat	nat-basic	s
abs	int-abs	f	Int → Int
i	intnat	v	Int
i→n	intnat	f	Int → Nat
j	intnat	v	Int
m	intnat	v	Nat
n	intnat	v	Nat
n→i	intnat	f	Nat → Int