[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
# .	list-data	f	List → Nat
#oc	list-perm	f	Elem × List → Nat
. '	list	f	Elem → List
. ( . )	list-getput	pf	List × Nat → Elem with λ x, n. n < # x
. ( . := . )	list-getput	pf	List × Nat × Elem → List with λ x, n, a. n < # x
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	Elem × List → List
. + .	list	f	List × List → List
. + .	list	f	List × Elem → List
. ++ .	list-dup	f	List × Elem → List
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	Elem × Elem → List
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List × Elem → List
. -l .	list-del	f	List × Elem → List
. -p .	list-del	f	List × Nat → List
. < .	oelem	p	Elem × Elem
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List × List
. > .	nat	p	Nat × Nat
. \ .	list-set	f	List × List → List
. ∈ .	list	p	Elem × List
. ∪ .	list-set	f	List × List → List
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	list-set	p	List × List
. ⊆m .	list-perm	p	List × List
. ⊑ .	list-last	p	List × List
. ⊒ .	list-last	p	List × List
. butlast	list-last	pf	List → List with λ x. x ≠ []
. head	list-data	pf	List → Elem with λ x. x ≠ []
. last	list-last	pf	List → Elem with λ x. x ≠ []
. tail	list-data	pf	List → List with λ x. x ≠ []
[]	list-data	c	List
Elem	elem	s
List	list-data	s
Nat	nat-basic	s
a	olist-min-max	v	Elem
all<	olist-min-max	p	List × Elem
all<	olist-min-max	p	List × Nat × Nat × Elem
all>	olist-min-max	p	List × Elem
all>	olist-min-max	p	List × Nat × Nat × Elem
all≤	olist-min-max	p	List × Elem
all≤	olist-min-max	p	List × Nat × Nat × Elem
all≥	olist-min-max	p	List × Elem
all≥	olist-min-max	p	List × Nat × Nat × Elem
butlastn	list-last	pf	Nat × List → List with λ n, x. n ≤ # x
count	filter-count	f	List × (Elem → Bool) → Nat
count	filter-count	pf	List × Nat × Nat × (Elem → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
disj	list-dup	p	List × List
dups	list-dup	p	List
fillfirst	list-last	f	Nat × Elem × List → List
filter	list-set	f	List × List → List
filter	filter-count	f	List × (Elem → Bool) → List
firstn	list-del	pf	Nat × List → List with λ n, x. n ≤ # x
frome	list-del	f	List × Elem → List
ins≤	olist	f	Elem × List → List
lastn	list-del	pf	Nat × List → List with λ n, x. n ≤ # x
max	oelem-min-max	f	Elem × Elem → Elem
max	olist-min-max	pf	List → Elem with λ x. x ≠ []
merge	olist	f	List × List → List
min	oelem-min-max	f	Elem × Elem → Elem
min	olist-min-max	pf	List → Elem with λ x. x ≠ []
mklist	list-last	f	Elem × Nat → List
ordered<	olist	p	List
ordered≤	olist	p	List
perm	list-perm	p	List × List
pos	list-del	f	Elem × List → Nat
restn	list-del	pf	Nat × List → List with λ n, x. n ≤ # x
rev	list-last	f	List → List
rmdup	list-dup	f	List → List
sort	olist-sort	f	List → List
sublist	list-del	pf	Nat × Nat × List → List with λ n, m, x. n + m ≤ # x
x	olist-min-max	v	List