Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	Array[A] → Nat
. ( . )	array	pf	Array[A] × Nat → A with λ ar, n. n < # ar
. ( . := . )	array	pf	Array[A] × Nat × A → Array[A] with λ ar, n, a. n < # ar
. + .	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
Array	array	s
Nat	nat-basic	s
ar	get-outside	v	Array[A]
mkarray	array	f	Nat → Array[A]
mkarray	array	f	Nat × A → Array[A]
n	get-outside	v	Nat