| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | partition | f | partition → nat |
| . ' | partition | f | partelem → partition |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | partition | f | partelem × partelem → partition |
| . + . | partition | f | partelem × partition → partition |
| . + . | partition | f | partition × partelem → partition |
| . + . | partition | f | partition × partition → partition |
| . ++ . | partition | f | partition × partelem → partition |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | partition | f | partition × nat → partition |
| . -1l . | partition | f | partition × partelem → partition |
| . -l . | partition | f | partition × partelem → partition |
| . .butlast | partition | f | partition → partition |
| . .count | partelem | f | partelem → nat |
| . .count:= . | partelem | f | partelem × nat → partelem |
| . .first | partelem | f | partelem → nat |
| . .first:= . | partelem | f | partelem × nat → partelem |
| . .head | partition | f | partition → partelem |
| . .last | partelem | f | partelem → nat |
| . .last | partition | f | partition → partelem |
| . .last:= . | partelem | f | partelem × nat → partelem |
| . .tail | partition | f | partition → partition |
| . < . | partition | p | partition × partition |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | partition | f | partition × nat → partelem |
| . [ . ] | partition | f | partition × nat × partelem → partition |
| . ∈ . | partition | p | partelem × partition |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | partition | p | partition × partition |
| . ⊒ . | partition | p | partition × partition |
| [] | partition | c | partition |
| P | partition | v | partition |
| P0 | partition | v | partition |
| P1 | partition | v | partition |
| P10 | partition | v | partition |
| P2 | partition | v | partition |
| P3 | partition | v | partition |
| P4 | partition | v | partition |
| P5 | partition | v | partition |
| P6 | partition | v | partition |
| P7 | partition | v | partition |
| P8 | partition | v | partition |
| P9 | partition | v | partition |
| butlastn | partition | f | nat × partition → partition |
| disj | partition | p | partition × partition |
| dups | partition | p | partition |
| fillfirst | partition | f | nat × partelem × partition → partition |
| firstn | partition | f | nat × partition → partition |
| frome | partition | f | partition × partelem → partition |
| lastn | partition | f | nat × partition → partition |
| m | nat-basic2 | v | nat |
| m0 | partelem | v | nat |
| m1 | partelem | v | nat |
| m2 | partelem | v | nat |
| m3 | partelem | v | nat |
| m4 | partelem | v | nat |
| mklist | partition | f | partelem × nat → partition |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| p | partelem | v | partelem |
| p0 | partition | v | partelem |
| p1 | partition | v | partelem |
| p2 | partition | v | partelem |
| partelem | partelem | s | |
| partition | partition | s | |
| pe | partelem | f | nat × nat × nat → partelem |
| pos | partition | f | partelem × partition → nat |
| restn | partition | f | nat × partition → partition |
| rev | partition | f | partition → partition |
| rmdup | partition | f | partition → partition |
| sublist | partition | f | nat × nat × partition → partition |