[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
# .arrayfarray → nat
#ocnatarrayfnat × array → nat
. 'natarrayfnat → array
. + .nat-basicfnat × nat → nat
. + .list-as-arrayinstancefarray × array → array
. + .natarrayfarray × nat → array
. + .natarrayfnat × array → array
. ++ .natarrayfarray × nat → array
. +1nat-basicfnat → nat
. +2 .natarrayfnat × nat → array
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. -1l .natarrayfarray × nat → array
. -l .natarrayfarray × nat → array
. -p .list-as-arrayinstancefarray × nat → array
. .butlastlist-as-arrayinstancepfarray → array with λ x. x ≠ []
. .firstnatarraypfarray → nat with λ ar. ar ≠ []
. .lastnatarraypfarray → nat with λ x. x ≠ []
. .restarray-listopspfarray → array with λ ar. ar ≠ []
. < .nat-basicpnat × nat
. < .array-listopsparray × array
. > .natpnat × nat
. [ . ]natarraypfarray × nat → nat with λ ar, n. n < # ar
. [ . ]natarraypfarray × nat × nat → array with λ ar, n, a. n < # ar
. \ .list-as-arrayinstancefarray × array → array
. ∈ .natarraypnat × array
. ∪ .list-as-arrayinstancefarray × array → array
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .list-as-arrayinstanceparray × array
. ⊆m .list-as-arrayinstanceparray × array
. ⊑ .list-as-arrayinstanceparray × array
. ⊒ .list-as-arrayinstanceparray × array
[]array-listopscarray
arrayarrays
butlastnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
cmpnatarrayparray × nat
cmparray-copypparray × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmpnatarraypparray × nat × nat × nat with λ ar, a, m, n. m + n ≤ # ar
copyarray-copypfarray × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
disjlist-as-arrayinstanceparray × array
dupslist-as-arrayinstanceparray
fillnatarrayfarray × nat → array
fillnatarraypfarray × nat × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fillfirstnatarrayfnat × nat × array → array
filterlist-as-arrayinstancefarray × array → array
firstnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
fromenatarrayfarray × nat → array
id○array-copyparray × array × nat
id○array-copyparray × array × nat × nat
idrangearray-copypparray × nat × nat with λ ar, m, n. m + n ≤ # ar
ins≤natarrayfnat × array → array
lastnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
mergeoarray-sortfarray × array → array
mkarrayarrayfnat → array
mklistnatarrayfnat × nat → array
natnat-basics
ordered<oarray-sortparray
ordered≤oarray-sortparray
permlist-as-arrayinstanceparray × array
posnatarrayfnat × array → nat
restnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
revlist-as-arrayinstancefarray → array
rmduplist-as-arrayinstancefarray → array
subarrayarray-copypfarray × nat × nat → array with λ ar, m, n. m + n ≤ # ar
sublistlist-as-arrayinstancepfnat × nat × array → array with λ n, m, x. n + m ≤ # x