Signature symbols in this unit

Symbol	Specification	Kind	Type
#c .	matrix	f	Matrix → Nat
#r .	matrix	f	Matrix → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. < .	nat-basic	p	Nat × Nat
. > .	nat	p	Nat × Nat
. [ . ]	matrix	pf	Matrix × Nat × Nat → Elem with λ mx, r, c. r < #r mx ∧ c < #c mx
. [ . ]	matrix	pf	Matrix × Nat × Nat × Elem → Matrix with λ mx, r, c, a. r < #r mx ∧ c < #c mx
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
Elem	elem	s
Matrix	matrix	s
Nat	nat-basic	s
a	matrix	v	Elem
b	matrix	v	Elem
c	matrix	v	Nat
mkmatrix	matrix	f	Nat × Nat × Elem → Matrix
mx	matrix	v	Matrix
r	matrix	v	Nat