| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # | rawcontext | f | rawctxt → nat |
| # | 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 | rawcontext | f | rawctxt → term |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . _ . | term | f | term × term → term |
| . _ . | rawcontext | f | rawctxt × term → rawctxt |
| . _ . | rawcontext | f | term × rawctxt → rawctxt |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| .c | rawcontext | f | rawctxt → rawctxt |
| ap | term | p | term |
| C | rawcontext | v | rawctxt |
| C0 | rawcontext | v | rawctxt |
| Ca | rawcontext | p | rawctxt |
| Cf | rawcontext | p | rawctxt |
| context | context | p | rawctxt |
| 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 | |
| O | rawcontext | c | rawctxt |
| rawctxt | rawcontext | s | |
| S | term | c | term |
| t | term | v | term |
| t0 | term | v | term |
| t1 | term | v | term |
| t2 | term | v | term |
| term | term | s | |
| value | value | p | term |