| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # | term | f | term → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . .1 | term | f | term → term |
| . .2 | term | f | term → term |
| . .t | term_or_none | f | term_or_none → term |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . _ . | term | f | term × term → term |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| ap | term | p | term |
| K | term | c | term |
| m | nat-basic2 | v | nat |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| none | term_or_none | c | term_or_none |
| S | term | c | term |
| some | term_or_none | f | term → term_or_none |
| t | term | v | term |
| t0 | term | v | term |
| t1 | term | v | term |
| t2 | term | v | term |
| term | term | s | |
| term_or_none | term_or_none | s | |
| tn | term_or_none | v | term_or_none |