| Symbol | Specification | Kind | Type |
|---|
| # . | laddress-list | f | laddress-list → nat |
| . ' | laddress-list | f | laddress → laddress-list |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | laddress-list | f | laddress-list × laddress → laddress-list |
| . + . | laddress-list | f | laddress × laddress-list → laddress-list |
| . + . | laddress-list | f | laddress-list × laddress-list → laddress-list |
| . ++ . | laddress-list | f | laddress-list × laddress → laddress-list |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | laddress-list | f | laddress × laddress → laddress-list |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | laddress-list | f | laddress-list × laddress → laddress-list |
| . -l . | laddress-list | f | laddress-list × laddress → laddress-list |
| . -p . | laddress-list | f | laddress-list × nat → laddress-list |
| . .butlast | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . .head | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .last | laddress-list | pf | laddress-list → laddress with λ lax. lax ≠ [] |
| . .off | laddress | f | laddress → nat |
| . .off:= . | laddress | f | laddress × nat → laddress |
| . .size | laddress | f | laddress → nat |
| . .size:= . | laddress | f | laddress × nat → laddress |
| . .tail | laddress-list | pf | laddress-list → laddress-list with λ lax. lax ≠ [] |
| . < . | nat-basic | p | nat × nat |
| . < . | laddress-list | p | laddress-list × laddress-list |
| . > . | nat | p | nat × nat |
| . [ . ] | laddress-list | pf | laddress-list × nat × laddress → laddress-list with λ lax, n, ladr. n < # lax |
| . [ . ] | laddress-list | pf | laddress-list × nat → laddress with λ lax, n. n < # lax |
| . ∈ . | laddress-list | p | laddress × laddress-list |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | laddress-list | p | laddress-list × laddress-list |
| . ⊒ . | laddress-list | p | laddress-list × laddress-list |
| @ | laddress | f | nat × nat → laddress |
| [] | laddress-list | c | laddress-list |
| butlastn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| disj | laddress-list | p | laddress-list × laddress-list |
| dropn | laddress-list | f | nat × laddress-list → laddress-list |
| dups | laddress-list | p | laddress-list |
| fillfirst | laddress-list | f | nat × laddress × laddress-list → laddress-list |
| firstn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| frome | laddress-list | f | laddress-list × laddress → laddress-list |
| laddress | laddress | s | |
| laddress-list | laddress-list | s | |
| ladr | laddress | v | laddress |
| ladr0 | laddress-list | v | laddress |
| ladr1 | laddress-list | v | laddress |
| ladr2 | laddress-list | v | laddress |
| lastn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| lax | laddress-list | v | laddress-list |
| lax0 | laddress-list | v | laddress-list |
| lax1 | laddress-list | v | laddress-list |
| lax2 | laddress-list | v | laddress-list |
| lax3 | laddress-list | v | laddress-list |
| m | nat-basic | v | nat |
| m0 | laddress | v | nat |
| m1 | laddress | v | nat |
| m2 | laddress | v | nat |
| mklist | laddress-list | f | laddress × nat → laddress-list |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| pos | laddress-list | f | laddress × laddress-list → nat |
| prefixn | laddress-list | f | nat × laddress-list → laddress-list |
| restn | laddress-list | pf | nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax |
| rev | laddress-list | f | laddress-list → laddress-list |
| rmdup | laddress-list | f | laddress-list → laddress-list |
| slice | laddress-list | f | nat × nat × laddress-list → laddress-list |
| sublist | laddress-list | pf | nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax |