| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | array | f | array → nat |
| # . | list-data | f | list → nat |
| #oc | boollist | f | bool × list → nat |
| . ' | boollist | f | bool → list |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | boollist | f | bool × list → list |
| . + . | boollist | f | bool × bool → list |
| . + . | list | f | list × list → list |
| . + . | boollist | f | list × bool → list |
| . ++ . | boollist | f | list × bool → list |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | list-del | f | list × nat → list |
| . -1l . | boollist | f | list × bool → list |
| . -l . | boollist | f | list × bool → list |
| . .butlast | list-last | f | list → list |
| . .first | boollist | p | list |
| . .last | boollist | p | list |
| . .rest | list-data | f | list → list |
| . < . | list-data | p | list × list |
| . < . | nat-basic1 | p | nat × nat |
| . < . | boollist | p | bool × bool |
| . > . | nat | p | nat × nat |
| . [ . ] | boolarr | f | array × nat × bool → array |
| . [ . ] | boollist | p | list × nat |
| . [ . ] | boollist | f | list × nat × bool → list |
| . [ . ] | boolarr | p | array × nat |
| . \ . | list-set | f | list × list → list |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ∈ . | boollist | p | bool × list |
| . ∪ . | list-set | f | list × list → list |
| . ⊆ . | list-set | p | list × list |
| . ⊆m . | list-perm | p | list × list |
| . ⊑ . | list-last | p | list × list |
| . ⊒ . | list-last | p | list × list |
| [] | list-data | c | list |
| ar | array | v | array |
| ar0 | array | v | array |
| ar1 | array | v | array |
| ar2 | array | v | array |
| arr2list | arr2list | f | array × nat → list |
| array | array | s | |
| bool | boollist | s | |
| butlastn | list-last | f | nat × list → list |
| bv | boollist | v | bool |
| bv0 | boollist | v | bool |
| bv1 | boollist | v | bool |
| bv2 | boollist | v | bool |
| disj | list-dup | p | list × list |
| dups | list-dup | p | list |
| fillfirst | boollist | f | nat × bool × list → list |
| filter | list-set | f | list × list → list |
| firstn | list-del | f | nat × list → list |
| frome | boollist | f | list × bool → list |
| ins≤ | boollist | f | bool × list → list |
| isperm | arr2list | p | array × array |
| issorted | arr2list | p | array |
| lastn | list-del | f | nat × list → list |
| list | list-data | s | |
| m | nat-basic2 | v | nat |
| merge | olist | f | list × list → list |
| mkarray | array | f | nat → array |
| mklist | boollist | f | bool × nat → list |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| ordered< | olist | p | list |
| ordered≤ | olist | p | list |
| perm | list-perm | p | list × list |
| pos | boolarr | f | array × bool → nat |
| pos | boollist | f | bool × list → nat |
| restn | list-del | f | nat × list → list |
| rev | list-last | f | list → list |
| rmdup | list-dup | f | list → list |
| sort | olist-sort | f | list → list |
| sublist | list-del | f | nat × nat × list → list |
| x | list-data | v | list |
| x0 | list-data | v | list |
| x1 | list-data | v | list |
| x2 | list-data | v | list |
| y | list-data | v | list |
| y0 | list-data | v | list |
| y1 | list-data | v | list |
| y2 | list-data | v | list |
| z | list-data | v | list |
| z0 | list-data | v | list |
| z1 | list-data | v | list |
| z2 | list-data | v | list |