Signature symbols in this unit

Symbol	Specification	Kind	Type
. * .	matrix-dot	f	matrix × matrix → matrix
. * .	int-mult	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. +1	nat-basic1	f	nat → nat
. +1	int-basic1	f	int → int
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1	int-basic1	f	int → int
. .cols	matrix	f	matrix → nat
. .rows	matrix	f	matrix → nat
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	int-abs	p	int × int
. > .	nat	p	nat × nat
. [ . ]	matrix	f	matrix × nat × nat → int
. [ . ]	matrix	f	matrix × nat × nat × int → matrix
. × .	matrix	f	nat × nat → matrix
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
~ .	int-abs	f	int → int
Σ	matrix-dot	f	nat × (nat → int) → int
A	matrix	v	matrix
B	matrix	v	matrix
C	matrix	v	matrix
abs	int-abs	f	int → int
i	int-basic1	v	int
i0	int-basic1	v	int
int	int-basic1	s
j	int-basic1	v	int
j0	int-basic1	v	int
k	matrix-dot	v	nat
m	nat-basic1	v	nat
m0	matrix	v	nat
matrix	matrix	s
multiply	multiply	pr	matrix × matrix : matrix
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
nf	matrix-dot	v	nat → int
nnf	matrix-dot	v	nat × nat → int