[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	array('a) → nat
#c .	matrix	f	matrix('a) → nat
#oc	list-as-arrayinstance	f	'a × array('a) → nat
#r .	matrix	f	matrix('a) → nat
. '	list-as-arrayinstance	f	'a → array('a)
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	list-as-arrayinstance	f	array('a) × array('a) → array('a)
. + .	list-as-arrayinstance	f	array('a) × 'a → array('a)
. + .	array-listops	f	'a × array('a) → array('a)
. ++ .	list-as-arrayinstance	f	array('a) × 'a → array('a)
. +1	nat-basic	f	nat → nat
. +2 .	list-as-arrayinstance	f	'a × 'a → array('a)
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	list-as-arrayinstance	f	array('a) × 'a → array('a)
. -l .	list-as-arrayinstance	f	array('a) × 'a → array('a)
. -p .	list-as-arrayinstance	f	array('a) × nat → array('a)
. .butlast	list-as-arrayinstance	pf	array('a) → array('a) with λ x. x ≠ []
. .first	array-listops	pf	array('a) → 'a with λ ar. ar ≠ []
. .foldLeft ( . )	list-as-arrayinstance	f	array('a) × 'b × ('b × 'a → 'b) → 'b
. .last	list-as-arrayinstance	pf	array('a) → 'a with λ x. x ≠ []
. .rest	array-listops	pf	array('a) → array('a) with λ ar. ar ≠ []
. .toArc	rowcol-upd	f	matrix('a) → array('a)
. .toArr	rowcol-upd	f	matrix('a) → array('a)
. < .	nat-basic	p	nat × nat
. < .	array-listops	p	array('a) × array('a)
. < .	tord	p	tord × tord
. > .	nat	p	nat × 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
. [ . ]	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
. [ . ]c	matrix+array	pf	matrix('a) × nat → array('a) with λ mx, c. c < #c mx
. [ . ]c	rowcol-upd	pf	matrix('a) × nat × array('a) → matrix('a) with λ mx, c, a. c < #c mx ∧ # a = #r mx
. [ . ]r	matrix+array	pf	matrix('a) × nat → array('a) with λ mx, r. r < #r mx
. [ . ]r	rowcol-upd	pf	matrix('a) × nat × array('a) → matrix('a) with λ mx, r, a. r < #r mx ∧ # a = #c mx
. [ . ]rv	matrix-revops	pf	matrix('a) × nat × nat → 'a with λ mx, c, r. c < #c mx ∧ r < #r mx
. [ . ]rv	matrix-revops	pf	matrix('a) × nat × nat × 'a → matrix('a) with λ mx, c, r, a. c < #c mx ∧ r < #r mx
. \ .	list-as-arrayinstance	f	array('a) × array('a) → array('a)
. ∈ .	list-as-arrayinstance	p	'a × array('a)
. ∪ .	list-as-arrayinstance	f	array('a) × array('a) → array('a)
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	list-as-arrayinstance	p	array('a) × array('a)
. ⊆m .	list-as-arrayinstance	p	array('a) × array('a)
. ⊑ .	list-as-arrayinstance	p	array('a) × array('a)
. ⊒ .	list-as-arrayinstance	p	array('a) × array('a)
. map .	list-as-arrayinstance	f	array('a) × ('a → 'b) → array('b)
[]	array-listops	c	array('a)
C	Bubblesort-col	v	nat,flexible
MX	Bubblesort-col	v	matrix(tord),flexible
N	Bubblesort-col	v	nat,flexible
R	Bubblesort-col	v	nat,flexible
a	Bubblesort-col	v	tord
all<	oarray-sort	p	array(tord) × tord
all<	oarray-sort	p	array(tord) × nat × nat × tord
all>	oarray-sort	p	array(tord) × tord
all>	oarray-sort	p	array(tord) × nat × nat × tord
all≤	oarray-sort	p	array(tord) × tord
all≤	oarray-sort	p	array(tord) × nat × nat × tord
all≥	oarray-sort	p	array(tord) × tord
all≥	oarray-sort	p	array(tord) × nat × nat × tord
ar	Bubblesort-col	v	array(tord)
array	array	s
butlastn	list-as-arrayinstance	pf	nat × array('a) → array('a) with λ n, x. n ≤ # x
cmp	array-copy	p	array('a) × 'a
cmp	array-copy	pp	array('a) × nat × array('a) × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	array('a) × 'a × nat × nat with λ ar, a, m, n. m + n ≤ # ar
copy	array-copy	pf	array('a) × nat × array('a) × nat × nat → array('a) with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
count	oarray-sort	f	array('a) × ('a → bool) → nat
count	oarray-sort	pf	array('a) × nat × nat × ('a → bool) → nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
disj	list-as-arrayinstance	p	array('a) × array('a)
dups	list-as-arrayinstance	p	array('a)
fill	array-copy	f	array('a) × 'a → array('a)
fill	array-copy	pf	array('a) × 'a × nat × nat → array('a) with λ ar, a, n, m. n + m ≤ # ar
fillfirst	list-as-arrayinstance	f	nat × 'a × array('a) → array('a)
filter	list-as-arrayinstance	f	array('a) × array('a) → array('a)
filter	oarray-sort	f	array('a) × ('a → bool) → array('a)
firstn	list-as-arrayinstance	pf	nat × array('a) → array('a) with λ n, x. n ≤ # x
frome	list-as-arrayinstance	f	array('a) × 'a → array('a)
id○	array-copy	p	array('a) × array('a) × nat
id○	array-copy	p	array('a) × array('a) × nat × nat
idrange	array-copy	pp	array('a) × nat × nat with λ ar, m, n. m + n ≤ # ar
ins≤	oarray-sort	f	tord × array(tord) → array(tord)
lastn	list-as-arrayinstance	pf	nat × array('a) → array('a) with λ n, x. n ≤ # x
matrix	matrix	s
max	tord-min-max	f	tord × tord → tord
max	oarray-sort	pf	array(tord) → tord with λ x. x ≠ []
merge	oarray-sort	f	array(tord) × array(tord) → array(tord)
min	tord-min-max	f	tord × tord → tord
min	oarray-sort	pf	array(tord) → tord with λ x. x ≠ []
mkarray	array	f	nat → array('a)
mklist	list-as-arrayinstance	f	'a × nat → array('a)
mkmatrix	matrix	f	nat × nat × 'a → matrix('a)
mx	Bubblesort-col	v	matrix(tord)
n	Bubblesort-col	v	nat
nat	nat-basic	s
ordered<	oarray-sort	p	array(tord)
ordered≤	oarray-sort	p	array(tord)
perm	list-as-arrayinstance	p	array('a) × array('a)
pos	list-as-arrayinstance	f	'a × array('a) → nat
psortcol#	Bubblesort-col	pr	nat : matrix(tord)
restn	list-as-arrayinstance	pf	nat × array('a) → array('a) with λ n, x. n ≤ # x
rev	list-as-arrayinstance	f	array('a) → array('a)
rmdup	list-as-arrayinstance	f	array('a) → array('a)
sort	oarray-sort	f	array(tord) → array(tord)
subarray	array-copy	pf	array('a) × nat × nat → array('a) with λ ar, m, n. m + n ≤ # ar
sublist	list-as-arrayinstance	pf	nat × nat × array('a) → array('a) with λ n, m, x. n + m ≤ # x
toArc	rowcol-upd	f	matrix('a) × nat → array('a)
toArr	rowcol-upd	f	matrix('a) × nat → array('a)
tord	tord	s