[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
# .list-of-natarrayflist-of-natarray → nat
#ocnatarrayfnat × array → nat
. 'natarrayfnat → array
. 'list-of-natarrayfarray → list-of-natarray
. + .nat-basicfnat × nat → nat
. + .list-as-arrayinstancefarray × array → array
. + .natarrayfarray × nat → array
. + .natarrayfnat × array → array
. + .list-of-natarrayfarray × list-of-natarray → list-of-natarray
. + .list-of-natarrayflist-of-natarray × list-of-natarray → list-of-natarray
. + .list-of-natarrayflist-of-natarray × array → list-of-natarray
. ++ .natarrayfarray × nat → array
. ++ .list-of-natarrayflist-of-natarray × array → list-of-natarray
. +1nat-basicfnat → nat
. +2 .natarrayfnat × nat → array
. +2 .list-of-natarrayfarray × array → list-of-natarray
. - .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 ≠ []
. .butlastlist-of-natarraypflist-of-natarray → list-of-natarray with λ x. x ≠ []
. .firstnatarraypfarray → nat with λ ar. ar ≠ []
. .headlist-of-natarraypflist-of-natarray → array with λ x. x ≠ []
. .lastnatarraypfarray → nat with λ x. x ≠ []
. .lastlist-of-natarraypflist-of-natarray → array with λ x. x ≠ []
. .restarray-listopspfarray → array with λ ar. ar ≠ []
. .taillist-of-natarraypflist-of-natarray → list-of-natarray with λ x. x ≠ []
. < .nat-basicpnat × nat
. < .array-listopsparray × array
. < .list-of-natarrayplist-of-natarray × list-of-natarray
. > .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-of-natarrayparray × list-of-natarray
. ∪ .list-as-arrayinstancefarray × array → array
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .list-as-arrayinstanceparray × array
. ⊆m .list-as-arrayinstanceparray × array
. ⊑ .list-as-arrayinstanceparray × array
. ⊑ .list-of-natarrayplist-of-natarray × list-of-natarray
. ⊒ .list-as-arrayinstanceparray × array
. ⊒ .list-of-natarrayplist-of-natarray × list-of-natarray
[]array-listopscarray
[]list-of-natarrayclist-of-natarray
arrayarrays
butlastnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
butlastnlist-of-natarraypfnat × list-of-natarray → list-of-natarray 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
disjlist-of-natarrayplist-of-natarray × list-of-natarray
dupslist-as-arrayinstanceparray
dupslist-of-natarrayplist-of-natarray
fillnatarrayfarray × nat → array
fillnatarraypfarray × nat × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fillfirstnatarrayfnat × nat × array → array
fillfirstlist-of-natarrayfnat × array × list-of-natarray → list-of-natarray
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
list-of-natarraylist-of-natarrays
mergeoarray-sortfarray × array → array
mkarrayarrayfnat → array
mklistnatarrayfnat × nat → array
mklistlist-of-natarrayfarray × nat → list-of-natarray
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
revlist-of-natarrayflist-of-natarray → list-of-natarray
rmduplist-as-arrayinstancefarray → array
rmduplist-of-natarrayflist-of-natarray → list-of-natarray
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