| Symbol | Specification | Kind | Type |
|---|
| # . | address-list-set | f | address-set → nat |
| # . | address-list-set | f | address-list → nat |
| . ' | address-list-set | f | address → address-list |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | address-list-set | f | address × address-list → address-list |
| . + . | address-list-set | f | address-list × address → address-list |
| . + . | address-list-set | f | address-list × address-list → address-list |
| . ++ . | address-list-set | f | address-set × address → address-set |
| . ++ . | address-list-set | f | address-list × address → address-list |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | address-list-set | f | address × address → address-list |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | address-list-set | f | address-set × address → address-set |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | address-list-set | f | address-list × address → address-list |
| . -l . | address-list-set | f | address-list × address → address-list |
| . -p . | address-list-set | f | address-list × nat → address-list |
| . .butlast | address-list-set | pf | address-list → address-list with λ ax. ax ≠ [] |
| . .head | address-list-set | pf | address-list → address with λ ax. ax ≠ [] |
| . .last | address-list-set | pf | address-list → address with λ ax. ax ≠ [] |
| . .tail | address-list-set | pf | address-list → address-list with λ ax. ax ≠ [] |
| . .toSet | address-list-set | f | address-list → address-set |
| . < . | address-list-set | p | address-list × address-list |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | address-list-set | pf | address-list × nat × address → address-list with λ ax, n, adr. n < # ax |
| . [ . ] | address-list-set | pf | address-list × nat → address with λ ax, n. n < # ax |
| . \ . | address-list-set | f | address-set × address-set → address-set |
| . ∈ . | address-list-set | p | address × address-set |
| . ∈ . | address-list-set | p | address × address-list |
| . ∩ . | address-list-set | f | address-set × address-set → address-set |
| . ∪ . | address-list-set | f | address-set × address-set → address-set |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | address-list-set | p | address-set × address-set |
| . ⊑ . | address-list-set | p | address-list × address-list |
| . ⊒ . | address-list-set | p | address-list × address-list |
| [] | address-list-set | c | address-list |
| { . } | address-list-set | f | address → address-set |
| ∅ | address-list-set | c | address-set |
| address | address | s | |
| address-list | address-list-set | s | |
| address-set | address-list-set | s | |
| adr | address | v | address |
| adr0 | address | v | address |
| adr1 | address | v | address |
| adr2 | address | v | address |
| adr3 | address | v | address |
| adr4 | address | v | address |
| adr5 | address | v | address |
| as | address-list-set | v | address-set |
| as0 | address-list-set | v | address-set |
| as1 | address-list-set | v | address-set |
| as2 | address-list-set | v | address-set |
| ax | address-list-set | v | address-list |
| ax0 | address-list-set | v | address-list |
| ax1 | address-list-set | v | address-list |
| ay | address-list-set | v | address-list |
| az | address-list-set | v | address-list |
| butlastn | address-list-set | pf | nat × address-list → address-list with λ n, ax. n ≤ # ax |
| disj | address-list-set | p | address-list × address-list |
| dropn | address-list-set | f | nat × address-list → address-list |
| dups | address-list-set | p | address-list |
| fillfirst | address-list-set | f | nat × address × address-list → address-list |
| firstn | address-list-set | pf | nat × address-list → address-list with λ n, ax. n ≤ # ax |
| frome | address-list-set | f | address-list × address → address-list |
| lastn | address-list-set | pf | nat × address-list → address-list with λ n, ax. n ≤ # ax |
| m | nat-basic | v | nat |
| mklist | address-list-set | f | address × nat → address-list |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| pos | address-list-set | f | address × address-list → nat |
| prefixn | address-list-set | f | nat × address-list → address-list |
| restn | address-list-set | pf | nat × address-list → address-list with λ n, ax. n ≤ # ax |
| rev | address-list-set | f | address-list → address-list |
| rmdup | address-list-set | f | address-list → address-list |
| slice | address-list-set | f | nat × nat × address-list → address-list |
| sublist | address-list-set | pf | nat × nat × address-list → address-list with λ n, m, ax. n + m ≤ # ax |