Signature symbols in this unit

Symbol	Specification	Kind	Type
#c .	matrix	f	Matrix[A] → Nat
#r .	matrix	f	Matrix[A] → Nat
. ( . )	matrix	pf	Matrix[A] × Nat × Nat → A with λ mx, r, c. r < #r mx ∧ c < #c mx
. ( . := . )	matrix	pf	Matrix[A] × Nat × Nat × A → Matrix[A] with λ mx, r, c, a. r < #r mx ∧ c < #c mx
. + .	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
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
Matrix	matrix	s
Nat	nat-basic	s
a	matrix	v	A
b	matrix	v	A
c	matrix	v	Nat
mkmatrix	matrix	f	Nat × Nat × A → Matrix[A]
mx	matrix	v	Matrix[A]
r	matrix	v	Nat