Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	Array → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. + .	array-listops	f	Elem × Array → Array
. +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
. .first	array-listops	pf	Array → Elem with λ ar. ar ≠ []
. .rest	array-listops	pf	Array → Array with λ ar. ar ≠ []
. < .	nat-basic	p	Nat × Nat
. < .	array-listops	p	Array × Array
. > .	nat	p	Nat × Nat
. [ . ]	array	pf	Array × Nat → Elem with λ ar, n. n < # ar
. [ . ]	array	pf	Array × Nat × Elem → Array with λ ar, n, a. n < # ar
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
[]	array-listops	c	Array
Array	array	s
Elem	elem	s
Nat	nat-basic	s
a	array-listops	v	Elem
ar	array-listops	v	Array
cmp	array-copy	p	Array × Elem
cmp	array-copy	pp	Array × Nat × Array × Nat × Nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	Array × Elem × Nat × Nat with λ ar, a, m, n. m + n ≤ # ar
copy	array-copy	pf	Array × Nat × Array × Nat × Nat → Array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
fill	array-copy	f	Array × Elem → Array
fill	array-copy	pf	Array × Elem × Nat × Nat → Array with λ ar, a, n, m. n + m ≤ # ar
id○	array-copy	p	Array × Array × Nat
id○	array-copy	p	Array × Array × Nat × Nat
idrange	array-copy	pp	Array × Nat × Nat with λ ar, m, n. m + n ≤ # ar
mkarray	array	f	Nat → Array
n	array-listops	v	Nat
subarray	array-copy	pf	Array × Nat × Nat → Array with λ ar, m, n. m + n ≤ # ar