| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | list_of_nat | f | natlist → nat |
| . ' | list_of_nat | f | nat → natlist |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | list_of_nat | f | natlist × nat → natlist |
| . + . | list_of_nat | f | nat × natlist → natlist |
| . + . | list_of_nat | f | natlist × natlist → natlist |
| . ++ . | list_of_nat | f | natlist × nat → natlist |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | list_of_nat | f | natlist × nat → natlist |
| . -l . | list_of_nat | f | natlist × nat → natlist |
| . -p . | list_of_nat | f | natlist × nat → natlist |
| . .butlast | list_of_nat | f | natlist → natlist |
| . .head | list_of_nat | f | natlist → nat |
| . .last | list_of_nat | f | natlist → nat |
| . .tail | list_of_nat | f | natlist → natlist |
| . < . | list_of_nat | p | natlist × natlist |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | list_of_nat | f | natlist × nat → nat |
| . [ . ] | list_of_nat | f | natlist × nat × nat → natlist |
| . ∈ . | list_of_nat | p | nat × natlist |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | list_of_nat | p | natlist × natlist |
| . ⊒ . | list_of_nat | p | natlist × natlist |
| . mktwo . | list_of_nat | f | nat × nat → natlist |
| [] | list_of_nat | c | natlist |
| X | list_of_nat | v | natlist |
| X0 | list_of_nat | v | natlist |
| X1 | list_of_nat | v | natlist |
| X10 | list_of_nat | v | natlist |
| X2 | list_of_nat | v | natlist |
| X3 | list_of_nat | v | natlist |
| X4 | list_of_nat | v | natlist |
| X5 | list_of_nat | v | natlist |
| X6 | list_of_nat | v | natlist |
| X7 | list_of_nat | v | natlist |
| X8 | list_of_nat | v | natlist |
| X9 | list_of_nat | v | natlist |
| butlastn | list_of_nat | f | nat × natlist → natlist |
| disj | list_of_nat | p | natlist × natlist |
| dups | list_of_nat | p | natlist |
| fillfirst | list_of_nat | f | nat × nat × natlist → natlist |
| firstn | list_of_nat | f | nat × natlist → natlist |
| frome | list_of_nat | f | natlist × nat → natlist |
| lastn | list_of_nat | f | nat × natlist → natlist |
| m | nat-basic2 | v | nat |
| mklist | list_of_nat | f | nat × nat → natlist |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| n2 | list_of_nat | v | nat |
| n3 | list_of_nat | v | nat |
| n4 | list_of_nat | v | nat |
| n5 | list_of_nat | v | nat |
| nat | nat-basic1 | s | |
| natlist | list_of_nat | s | |
| pos | list_of_nat | f | nat × natlist → nat |
| restn | list_of_nat | f | nat × natlist → natlist |
| rev | list_of_nat | f | natlist → natlist |
| rmdup | list_of_nat | f | natlist → natlist |
| sublist | list_of_nat | f | nat × nat × natlist → natlist |