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
. .1	nat-pair	f	nat → nat
. .1	int-pair	f	int → int
. .2	nat-pair	f	nat → nat
. .2	int-pair	f	int → int
. / .	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-pair	f	int × int → int
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
decode	int-pair	f	nat → int
decode	int-pair	f	int → nat
encode	nat-pair	f	nat × nat → nat
encode	int-pair	f	int → nat
encode	int-pair	f	nat → int
i	int-pair	v	int
i→n	intnat	f	int → nat
int	int-basic1	s
j	int-pair	v	int
m	int-pair	v	nat
maxenc	nat-pair	f	nat → nat
maxenc	nat-pair	f	nat × nat → nat
n	int-pair	v	nat
n→i	intnat	f	nat → int
nat	nat-basic	s