[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
#oclist-as-arrayinstancefelem × array → nat
. 'list-as-arrayinstancefelem → array
. + .list-as-arrayinstancefarray × array → array
. + .list-as-arrayinstancefarray × elem → array
. + .nat-basicfnat × nat → nat
. + .array-listopsfelem × array → array
. ++ .list-as-arrayinstancefarray × elem → array
. +1nat-basicfnat → nat
. +2 .list-as-arrayinstancefelem × elem → array
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. -1l .list-as-arrayinstancefarray × elem → array
. -l .list-as-arrayinstancefarray × elem → array
. -p .list-as-arrayinstancefarray × nat → array
. .butlastlist-as-arrayinstancepfarray → array with λ x. x ≠ []
. .firstarray-listopspfarray → elem with λ ar. ar ≠ []
. .lastlist-as-arrayinstancepfarray → elem with λ x. x ≠ []
. .restarray-listopspfarray → array with λ ar. ar ≠ []
. < .nat-basicpnat × nat
. < .array-listopsparray × array
. > .natpnat × nat
. [ . ]arraypfarray × nat → elem with λ ar, n. n < # ar
. [ . ]arraypfarray × nat × elem → array with λ ar, n, a. n < # ar
. \ .list-as-arrayinstancefarray × array → array
. ∈ .list-as-arrayinstancepelem × 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
cmparray-copyparray × elem
cmparray-copypparray × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmparray-copypparray × elem × 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
elemelems
fillarray-copyfarray × elem → array
fillarray-copypfarray × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fillfirstlist-as-arrayinstancefnat × elem × array → array
filterlist-as-arrayinstancefarray × array → array
firstnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
fromelist-as-arrayinstancefarray × elem → array
id○array-copyparray × array × nat
id○array-copyparray × array × nat × nat
idrangearray-copypparray × nat × nat with λ ar, m, n. m + n ≤ # ar
lastnlist-as-arrayinstancepfnat × array → array with λ n, x. n ≤ # x
mkarrayarrayfnat → array
mklistlist-as-arrayinstancefelem × nat → array
natnat-basics
permlist-as-arrayinstanceparray × array
poslist-as-arrayinstancefelem × 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