| Symbol | Specification | Kind | Type |
|---|---|---|---|
| . % . | int-div | pf | Int × Int → Int with λ i, j. j ≠ 0 |
| . * . | int-mult | f | Int × Int → Int |
| . + . | int-basic2 | f | Int × Int → Int |
| . +1 | int-basic1 | f | Int → Int |
| . - . | int-abs | f | Int × Int → Int |
| . -1 | int-basic1 | f | Int → Int |
| . / . | int-div | pf | Int × Int → Int with λ i, j. j ≠ 0 |
| . < . | int-basic1 | p | Int × Int |
| . > . | int-abs | p | Int × Int |
| . ^2 | int-square | f | Int → Int |
| . ≤ . | int-abs | p | Int × Int |
| . ≥ . | int-abs | p | Int × Int |
| ~ . | int-abs | f | Int → Int |
| Int | int-basic1 | s | |
| abs | int-abs | f | Int → Int |
| i | int-square | v | Int |
| j | int-square | v | Int |
| sqrt | int-square | pf | Int → Int with λ i. 0 ≤ i |