Rodin Handbook


2.5.6 Arithmetic

We have the usual operations on integers, $+$, $-$, $\cdot $ and $\div $ (ASCII: +, -, * and /). They can be compared with the usual equality operators: $<$, $\leq $, $\geq $, $>$ (ASCII: <, <=, >=, >).

$\mathord {\mathbb Z}$ (ASCII: INT) denotes the set of all integer numbers. $\mathord {\mathbb N}$ and $\mathord {\mathbb N}_1$ (ASCII: NAT and NAT1 respectively) are the subsets of natural numbers.


If you specify two variables $x$ and $y$ with $x\in \mathord {\mathbb Z}$ and $y\in \mathord {\mathbb N}$, then both are of type integer ($\mathord {\mathbb Z}$). $\mathord {\mathbb N}$ is not another type. There is just the additional condition $y \geq 0$.