Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	list-data	f	list → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	intlist	f	int → list
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	intlist	f	int × int → list
. + .	int-basic2	f	int × int → int
. + .	intlist	f	list × int → list
. + .	nat-basic2	f	nat × nat → nat
. + .	list	f	list × list → list
. + .	intlist	f	int × list → list
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. - .	int-abs	f	int × int → int
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. / .	nat-div	f	nat × nat → nat
. / .	int-div	f	int × int → int
. < .	list-data	p	list × list
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ∈ .	intlist	p	int × list
[]	list-data	c	list
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
d	intlist	v	int
h	intlist	v	int
head	intlist	f	list → int
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
int	int-basic1	s
j	int-basic1	v	int
j0	int-basic1	v	int
list	list-data	s
m	nat-basic2	v	nat
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pop	intlist	f	list → list
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list