Lesson 2  Integers
1. Introduction
Progress: 0%
This lesson teaches you the basics of operations over integers. If you have programming experience, you know most of these operators. So it should not take you long to finish this lesson. Do not skip this lesson, as some of the operators may still surprise you.
2. Integer literals
Progress: 11%
Code snippet:
// 0 is an integer literal
pure val int0 = 0
// 2 is an integer literal
pure val int1 = 2
// 3 is an integer literal
pure val negative1 = 3
Integer literals are written using the standard syntax: 0, 1, 1, 2, 2, ..., 314159265358979323846264338327950288419716939937510.
It is important to understand that Quint integers are big integers. There is neither a minimum integer, nor there is a maximum integer.
It's quite easy to express the standard 32bit, 64bit, 128bit, and 512bit integers with Quint integers. We will cover this in a follow up tutorial.
We omit several integer operators that produce sets. These operators are covered in the tutorial on sets.
3. Integer exponentiation
Progress: 22%
Code snippet:
// i^j is the integer exponentiation, that is,
// `i` multiplied by itself `j  1` times
pure def myPow(i, j) = i^j
We start with the exponentiation i^j
over integers,
which is also written as pow(i, j)
in many languages.
The result of i^j
is simply i
multiplied by itself j  1
times.
This is the first operator, as it lets us to write nice examples
in the following steps.
To get a better intuition at how i^j
works, run the following examples:
echo "2^32"  quint
echo "2^64"  quint
echo "2^256"  quint
echo "2^512"  quint
Exponentiation is not defined on all of its arguments. Try the following examples to get the intuition.
echo "(2)^3"  quint
echo "(2)^4"  quint
echo "2^(4)"  quint
echo "0^3"  quint
echo "0^0"  quint
echo "0^(2)"  quint
4. Integer addition
Progress: 33%
Code snippet:
// i + j is the integer addition
pure def myAdd(i, j) = i + j
We can add two integers by writing i + j
. Importantly, integers cannot
overflow, as they are big integers.
Try this simple example:
echo "2022 + 2023"  quint
It is important to remember that integer addition satisfies the laws of commutativity and associativity in Quint:
echo "11 + 17 == 17 + 11"  quint
echo "(11 + 17) + 19 == 11 + (17 + 19)"  quint
5. Integer subtraction
Progress: 44%
Code snippet:
// i  j is the integer subtraction
pure def mySub(i, j) = i  j
We can add two integers by writing i  j
.

Try this and see the result of the evaluation:
echo "2022  2023"  quint

Addition and subtraction have the same priority. Hence they are applied from left to right.
echo "11 + 13  17"  quint
Exercise: Is subtraction commutative?
6. Integer multiplication
Progress: 55%
Code snippet:
// i * j is the integer multiplication
pure def myMul(i, j) = i * j
We can multiply two integers by writing i * j
.
Remember that multiplication cannot produce any side effects like overflows:
echo "2^32 * 2^32 == 2^64"  quint
It is important to remember that integer multiplication satisfies the laws of commutativity and associativity in Quint:
echo "11 * 17 == 17 * 11"  quint
echo "(11 * 17) * 19 == 11 * (17 * 19)"  quint
7. Integer division and remainder
Progress: 66%
Code snippet:
// i / j is the integer division
pure def myDiv(i, j) = i / j
// i % j is the integer remainder
pure def myMod(i, j) = i % j
The operators i / j
and i % j
compute the integer part and the remainder
when dividing i
by j
, respectively. These operators have the following
property for all integer values of i
and all integer values of j != 0
:
i == (i / j) * j + i % j
.
Try the following examples to check your intuition:
echo "99 / 2 == 49"  quint
echo "99 % 2 == 1"  quint
echo "98 % 2 == 0"  quint
echo "((2^64  1) % 2^64 + 1) % 2^64"  quint
echo "(2^64  123) % 2^63"  quint
Exercise: Is division commutative?
8. Integer comparison
Progress: 77%
Code snippet:
// `i > j` is true if and only if `i` is greater than `j`
pure def myGreaterThan(i, j) = i > j
// `i >= j` is true if and only if `i` is greater than `j`, or equal to `j`
pure def myGreaterThanOrEqual(i, j) = i >= j
// `i < j` is true if and only if `i` is less than `j`
pure def myLessThan(i, j) = i < j
// `i <= j` is true if and only if `i` is less than `j`, or equal to `j`
pure def myLessThanOrEqual(i, j) = i <= j
// `i == j` is true if and only if `i` equals to `j`
pure def myEquals(i, j) = i == j
// `i != j` is true if and only if `i` is not equal to `j`
pure def myNotEqual(i, j) = i != j
These are the standard comparison operators that you know, for sure:
 Less than:
i < j
 Less than or equal:
i <= j
 Greater than:
i > j
 Greater than or equal:
i >= j
 Equals to:
i == j
 Not equal to:
i != j
Check your intuition by running the following examples:
echo "10 < 11"  quint
echo "10 < 10"  quint
echo "10 <= 11"  quint
echo "10 <= 10"  quint
echo "10 <= 9"  quint
echo "11 > 10"  quint
echo "10 > 10"  quint
echo "11 >= 10"  quint
echo "10 >= 10"  quint
echo "10 >= 9"  quint
echo "10 == 10"  quint
echo "10 == 11"  quint
echo "10 != 10"  quint
echo "10 != 11"  quint
9. Integer negation
Progress: 88%
Code snippet:
// i is the integer negation
pure def myUnaryMinus(i) = i
We almost forgot about the integer negation!
Not surprisingly, i
negates an integer i
.
Recall that Quint integers are big integers.
Hence, no overflow is possible.
Try a few examples:
echo "(3 + 2)"  quint
echo "(2^63) == 2^63"  quint
The end
You have made it!