| Symbol | Specification | Kind | Type |
|---|---|---|---|
| . % . | nat-div | f | nat × nat → nat |
| . % . | int-div | f | int × int → int |
| . * . | nat-mult | f | nat × nat → nat |
| . * . | int-mult | f | int × int → int |
| . + . | int-basic2 | f | int × int → int |
| . + . | nat-basic2 | f | nat × nat → nat |
| . +1 | int-basic1 | f | int → int |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . - . | int-abs | f | int × int → int |
| . -1 | int-basic1 | f | int → int |
| . -1 | nat-basic1 | f | nat → nat |
| . / . | int-div | f | int × int → int |
| . / . | nat-div | f | nat × nat → nat |
| . < . | nat-basic1 | p | nat × nat |
| . < . | int-basic1 | p | int × int |
| . > . | nat | p | nat × nat |
| . > . | int-abs | p | int × int |
| . ^ . | int-pot | f | int × int → int |
| . ^2 | int-square | f | int → int |
| . ≤ . | nat | p | nat × nat |
| . ≤ . | int-abs | p | int × int |
| . ≥ . | nat | p | nat × nat |
| . ≥ . | int-abs | p | int × int |
| ~ . | int-abs | f | int → int |
| abs | int-abs | f | int → int |
| even | int-min | p | int |
| i | int-basic1 | v | int |
| i→n | intnat | f | int → nat |
| i0 | int-basic1 | v | int |
| int | int-basic1 | s | |
| isSquare | int-square | p | int |
| j | int-basic1 | v | int |
| j0 | int-basic1 | v | int |
| m | nat-basic1 | v | nat |
| max | int-min | f | int × int → int |
| min | int-min | f | int × int → int |
| n | nat-basic1 | v | nat |
| n→i | intnat | f | nat → int |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| odd | int-min | p | int |
| sgn | int-min | f | int → int |
| sqrt | int-square | f | int → int |