| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | array_of_nat | f | arrnat → nat |
| #oc | array_of_nat | f | nat × arrnat × nat → nat |
| . + . | nat-basic2 | f | nat × nat → nat |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -1 | nat-basic1 | f | nat → nat |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | array_of_nat | f | arrnat × nat → nat |
| . [ . ] | array_of_nat | f | arrnat × nat × nat → arrnat |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| A | array_of_nat | v | arrnat |
| A0 | array_of_nat | v | arrnat |
| A1 | array_of_nat | v | arrnat |
| A2 | array_of_nat | v | arrnat |
| arrnat | array_of_nat | s | |
| m | nat-basic2 | v | nat |
| mkarray | array_of_nat | f | nat → arrnat |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| n2 | array_of_nat | v | nat |
| n3 | array_of_nat | v | nat |
| n4 | array_of_nat | v | nat |
| nat | nat-basic1 | s | |
| perm | array_of_nat | p | arrnat × arrnat |