[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-dataflist('a) → nat
#oclist-permf'a × list('a) → nat
. 'listf'a → list('a)
. + .nat-basicfnat × nat → nat
. + .list-dataf'a × list('a) → list('a)
. + .listflist('a) × list('a) → list('a)
. + .listflist('a) × 'a → list('a)
. ++ .list-dupflist('a) × 'a → list('a)
. +1nat-basicfnat → nat
. +2 .listf'a × 'a → list('a)
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. -1l .list-delflist('a) × 'a → list('a)
. -l .list-delflist('a) × 'a → list('a)
. -p .list-delflist('a) × nat → list('a)
. .butlastlist-lastpflist('a) → list('a) with λ x. x ≠ []
. .foldLeft ( . )listflist('a) × 'b × ('b × 'a → 'b) → 'b
. .headlist-datapflist('a) → 'a with λ x. x ≠ []
. .lastlist-lastpflist('a) → 'a with λ x. x ≠ []
. .taillist-datapflist('a) → list('a) with λ x. x ≠ []
. < .nat-basicpnat × nat
. < .list-dataplist('a) × list('a)
. < .weakordpweakord × weakord
. > .natpnat × nat
. [ . := . ]list-getputpflist('a) × nat × 'a → list('a) with λ x, n, a. n < # x
. [ . ]list-getputpflist('a) × nat → 'a with λ x, n. n < # x
. \ .list-setflist('a) × list('a) → list('a)
. ∈ .listp'a × list('a)
. ∪ .list-setflist('a) × list('a) → list('a)
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .list-setplist('a) × list('a)
. ⊆m .list-permplist('a) × list('a)
. ⊑ .list-lastplist('a) × list('a)
. ⊒ .list-lastplist('a) × list('a)
. map .listflist('a) × ('a → 'b) → list('b)
[]list-dataclist('a)
awolistvweakord
bwolistvweakord
butlastnlist-lastpfnat × list('a) → list('a) with λ n, x. n ≤ # x
cwolistvweakord
disjlist-dupplist('a) × list('a)
dupslist-dupplist('a)
fillfirstlist-lastfnat × 'a × list('a) → list('a)
filterlist-setflist('a) × list('a) → list('a)
firstnlist-delpfnat × list('a) → list('a) with λ n, x. n ≤ # x
fromelist-delflist('a) × 'a → list('a)
ins≤wolistfweakord × list(weakord) → list(weakord)
lastnlist-delpfnat × list('a) → list('a) with λ n, x. n ≤ # x
listlist-datas
mwolistvnat
mergewolistflist(weakord) × list(weakord) → list(weakord)
mklistlist-lastf'a × nat → list('a)
nwolistvnat
natnat-basics
ordered<wolistplist(weakord)
ordered≤wolistplist(weakord)
permlist-permplist('a) × list('a)
poslist-delf'a × list('a) → nat
restnlist-delpfnat × list('a) → list('a) with λ n, x. n ≤ # x
revlist-lastflist('a) → list('a)
rmduplist-dupflist('a) → list('a)
sublistlist-delpfnat × nat × list('a) → list('a) with λ n, m, x. n + m ≤ # x
weakordweakords
xwolistvlist(weakord)
ywolistvlist(weakord)
zwolistvlist(weakord)