| Symbol | Specification | Kind | Type |
|---|
| # . | natstream | f | natstream → natinf |
| # . | natstream | f | natlist → nat |
| . ' | natstream | f | nat → natlist |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | natstream | f | natstream × natstream → natstream |
| . + . | natstream | f | nat × natlist → natlist |
| . + . | natstream | f | nat × natstream → natstream |
| . + . | natstream | f | natlist × natlist → natlist |
| . + . | nat-inf | f | natinf × natinf → natinf |
| . + . | natstream | f | natlist × nat → natlist |
| . ++ . | natstream | f | natlist × nat → natlist |
| . +1 | nat-basic | f | nat → nat |
| . +l . | natstream | f | nat × nat → natlist |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | natstream | f | natlist × nat → natlist |
| . -l . | natstream | f | natlist × nat → natlist |
| . -pos . | natstream | f | natlist × nat → natlist |
| . .butlast | natstream | pf | natlist → natlist with λ nl. nl ≠ [] |
| . .f | natstream | pf | natstream → nat → nat with λ nσ. λ m. ∃ nnf. nσ = ⌜nnf⌝ |
| . .head | natstream | pf | natlist → nat with λ nl. nl ≠ [] |
| . .l | natstream | pf | natstream → natlist with λ nσ. finp(nσ) |
| . .last | natstream | pf | natlist → nat with λ nl. nl ≠ [] |
| . .n | nat-inf | pf | natinf → nat with λ n∞. n∞ ≠ ∞ |
| . .tail | natstream | pf | natlist → natlist with λ nl. nl ≠ [] |
| . < . | nat-basic | p | nat × nat |
| . < . | nat-inf | p | natinf × natinf |
| . < . | natstream | p | natlist × natlist |
| . > . | nat | p | nat × nat |
| . [ . ] | natstream | pf | natstream × nat × nat → natstream with λ nσ, n, m. finp(nσ) → ⌜n⌝ < # nσ |
| . [ . ] | natstream | pf | natstream × nat → nat with λ nσ, n. finp(nσ) → ⌜n⌝ < # nσ |
| . [ . ] | natstream | pf | natlist × nat × nat → natlist with λ nl, n, m. n < # nl |
| . [ . ] | natstream | pf | natlist × nat → nat with λ nl, n. n < # nl |
| . ∈ . | natstream | p | nat × natlist |
| . ≤ . | nat | p | nat × nat |
| . ≤ . | natstream | p | natstream × natstream |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | natstream | p | natstream × natstream |
| . ⊑ . | natstream | p | natlist × natlist |
| . ⊒ . | natstream | p | natlist × natlist |
| . from . | natstream | pf | natlist × nat → natlist with λ nl, n. n ≤ # nl |
| . from . | natstream | pf | natstream × nat → natstream with λ nσ, n. finp(nσ) → ⌜n⌝ < # nσ ∨ ⌜n⌝ = # nσ |
| . from . | natstream | f | (nat → nat) × nat → nat → nat |
| . to . | natstream | f | (nat → nat) × nat → natlist |
| . to . | natstream | pf | natlist × nat → natlist with λ nl, n. n ≤ # nl |
| . to . | natstream | pf | natstream × nat → natstream with λ nσ, n. finp(nσ) → ⌜n⌝ < # nσ ∨ ⌜n⌝ = # nσ |
| . to∞ . | natstream | pf | natstream × natinf → natstream with λ nσ, n∞. finp(nσ) → n∞ < # nσ ∨ n∞ = # nσ |
| [] | natstream | c | natlist |
| [] | natstream | c | natstream |
| ∞ | nat-inf | c | natinf |
| ⌜ . ⌝ | natstream | f | natlist → natstream |
| ⌜ . ⌝ | nat-inf | f | nat → natinf |
| ⌜ . ⌝ | natstream | f | (nat → nat) → natstream |
| butlastn | natstream | pf | nat × natlist → natlist with λ n, nl. n ≤ # nl |
| cnt | natstream | f | nat × natstream → natinf |
| disj | natstream | p | natlist × natlist |
| dups | natstream | p | natlist |
| fillfirst | natstream | f | nat × nat × natlist → natlist |
| filter | natstream | f | (nat → bool) × natstream → natstream |
| finp | natstream | p | natstream |
| firstn | natstream | pf | nat × natlist → natlist with λ n, nl. n ≤ # nl |
| frome | natstream | f | natlist × nat → natlist |
| hd | natstream | pf | natstream → nat with λ nσ. nσ ≠ [] |
| lastn | natstream | pf | nat × natlist → natlist with λ n, nl. n ≤ # nl |
| lastoc | natstream | f | nat × natstream → natinf |
| lim | natstream | pf | (nat → natstream) → natstream with λ nσf. mon(nσf) |
| m | nat-basic | v | nat |
| m0 | nat-inf | v | nat |
| m1 | natstream | v | nat |
| m2 | natstream | v | nat |
| m3 | natstream | v | nat |
| m4 | natstream | v | nat |
| min | nat-inf | f | natinf × natinf → natinf |
| mklist | natstream | f | nat × nat → natlist |
| mon | natstream | p | (nat → natstream) |
| n | nat-basic | v | nat |
| nσ | natstream | v | natstream |
| nσ0 | natstream | v | natstream |
| nσ1 | natstream | v | natstream |
| nσ2 | natstream | v | natstream |
| nσf | natstream | v | nat → natstream |
| n∞ | nat-inf | v | natinf |
| n∞0 | nat-inf | v | natinf |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| natinf | nat-inf | s | |
| natlist | natstream | s | |
| natstream | natstream | s | |
| nl | natstream | v | natlist |
| nl0 | natstream | v | natlist |
| nl1 | natstream | v | natlist |
| nl2 | natstream | v | natlist |
| nl5 | natstream | v | natlist |
| nnf | mon-lim-filter-count | v | nat → nat |
| nnf0 | natstream | v | nat → nat |
| nnf1 | natstream | v | nat → nat |
| np | mon-lim-filter-count | v | nat → bool |
| np0 | natstream | v | nat → bool |
| pos | natstream | f | nat × natlist → nat |
| rem | natstream | f | natstream × (nat → bool) → natstream |
| restn | natstream | pf | nat × natlist → natlist with λ n, nl. n ≤ # nl |
| rev | natstream | f | natlist → natlist |
| rmdup | natstream | f | natlist → natlist |
| sublist | natstream | pf | nat × nat × natlist → natlist with λ n, m, nl. n + m ≤ # nl |
| tl | natstream | pf | natstream → natstream with λ nσ. nσ ≠ [] |