| symbol | specification | entry |
|---|
| # | array | function,
array → nat |
| + | nat-basic2 | function,
nat × nat → nat |
| +1 | nat-basic1 | function,
nat → nat |
| - | nat | function,
nat × nat → nat |
| -1 | nat-basic1 | function,
nat → nat |
| < | nat-basic1 | predicate,
nat × nat |
| > | nat | predicate,
nat × nat |
| ] | nat-array | function,
array × nat → nat |
| ] | nat-array | function,
array × nat × nat → array |
| ] | array | function,
array × nat → elem |
| ] | array | function,
array × nat × elem → array |
| a | elem | variable,
elem |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| b | elem | variable,
elem |
| c | elem | variable,
elem |
| elem | elem | sort,
|
| m | nat-basic2 | variable,
nat |
| max | challenge1 | function,
array × nat × nat → nat |
| mkarray | array | function,
nat → array |
| n | nat-basic1 | variable,
nat |
| n0 | nat-basic1 | variable,
nat |
| n1 | nat-basic1 | variable,
nat |
| n2 | nat-array | variable,
nat |
| n3 | nat-array | variable,
nat |
| n4 | nat-array | variable,
nat |
| nat | nat-basic1 | sort,
|
| pos | nat-array | function,
array × nat → nat |
| pos | array | function,
array × elem → nat |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |