# Lesson 1 - Booleans

## 1. Introduction

*Progress:* 0%

In this lesson, you will learn how to use Booleans. It should take you real quick to learn this lesson.

**Do not skip this lesson.** It introduces a few important language concepts, not just the Booleans.

If you would like to see the complete code before diving into the details, check booleans.qnt.

## 2. Boolean literals

*Progress:* 6%

**Code snippet:**

```
// false is a built-in constant
pure val myFalse = false
// true is a built-in constant too
pure val myTrue = true
```

Quint has two built-in values of `bool`

type, called Boolean literals:

`false`

is the value that represents the value "false".`true`

is the value that represents the value "true".

Note that Quint is strict with respect to Boolean values.
There are only `false`

and `true`

. They are comparable
only to Boolean values, and there are no implicit conversions
from other types to the Boolean type.

You cannot modify Boolean values. You can carry them around as variable values, or in data structures.

Evaluate the Boolean literals in REPL:

`echo "false" | quint`

`echo "true" | quint`

## 3. Boolean negation

*Progress:* 13%

**Code snippet:**

```
// Boolean negation, which is written as `!x` in some languages
pure def myNot(x) = not(x)
```

The simplest operation we can do with a Boolean value is negation.

Evaluate the negation of `false`

and `true`

:

`echo "not(false)" | quint`

`echo "not(true)" | quint`

## 4. Boolean equality

*Progress:* 20%

**Code snippet:**

```
// you can compare Booleans for equality
pure def myEq(x, y) = x == y
```

We can compare Booleans for equality. The rules for equality are straightforward.

Try comparing `false`

and `true`

in all possible combinations:

`echo "false == false" | quint`

`echo "false == true" | quint`

`echo "true == false" | quint`

`echo "true == true" | quint`

One important feature of equality is that the arguments should have the same type. Hence, Booleans can be only compared to Booleans. The following expressions produces type errors. Try them:

`echo "false == 0" | quint`

`echo "true == 1" | quint`

## 5. Boolean inequality

*Progress:* 26%

**Code snippet:**

```
// you can compare Booleans for inequality
pure def myNeq(x, y) = x != y
```

We can compare Booleans for inequality. It is simply the opposite of `x == y`

.

Try comparing `false`

and `true`

in all possible combinations:

`echo "false != false" | quint`

`echo "false != true" | quint`

`echo "true != false" | quint`

`echo "true != true" | quint`

## 6. Dot form

*Progress:* 33%

**Code snippet:**

```
// you can also write negation like that
pure def myNot2(x) = x.not()
```

If you prefer object-oriented style, you can also write `x.not()`

. Try it out:

`echo "false.not()" | quint`

**This is a general principle:** You can write `foo(x)`

as `x.foo()`

and vice versa.

Be careful about not writing `false.not`

, as it would be understood as record access:

`echo "false.not" | quint`

## 7. Boolean "and"

*Progress:* 40%

**Code snippet:**

```
// Boolean "and", which is written as `x && y` in some languages
pure def myAnd(x, y) = x and y
```

Now it is time to learn about Boolean "and".

Evaluate all possible combinations of `false`

and `true`

:

`echo "false and false" | quint`

`echo "false and true" | quint`

`echo "true and false" | quint`

`echo "true and true" | quint`

## 8. Dot form for binary operators

*Progress:* 46%

**Code snippet:**

```
// You can also write Boolean "and" like that in the OOP form
pure def myAnd2(x, y) = x.and(y)
```

Similar to the operator `not`

, you can use the object-oriented form for
Boolean "and". Try it:

`echo "false.and(true)" | quint`

**This is a general principle:** You can replace `bar(x, y)`

with `x.bar(y)`

,
and vice versa.

This form may be useful with nested formulas like:

`x.and(y).and(z)`

## 9. And works for more than two arguments

*Progress:* 53%

**Code snippet:**

```
// We can apply "and" to more than two arguments
pure def myAnd3(x, y, z) = and(x, y, z)
```

As you see, "and" does not have to apply to two arguments only. You can use it with multiple arguments:

`echo "and(true, false, true)" | quint`

`echo "and(true, false, true, false)" | quint`

`echo "and(true, false, true, false, true)" | quint`

## 10. The and {...} form

*Progress:* 60%

**Code snippet:**

```
/// When your expressions get bigger, you can stack them in `and { ... }`
pure def myAnd4(x, y, z) = and {
x,
y,
z
}
```

Sometimes, we have to write complex expressions over Booleans. Yeah, that happens.

In this case, you can use the convenient form and { ... }, which is just syntax sugar for and(...).

Try it:

`echo "and { false == false, true == true }" | quint`

## 11. Boolean "or"

*Progress:* 66%

**Code snippet:**

```
// Boolean "or", which is written as `x || y` in some languages.
pure def myOr(x, y) = x or y
```

If there is "and", there must be "or".
Evaluate all possible combinations of `false`

and `true`

:

`echo "false or false" | quint`

`echo "false or true" | quint`

`echo "true or false" | quint`

`echo "true or true" | quint`

## 12. Other forms of "or"

*Progress:* 73%

**Code snippet:**

```
/// You can also write Boolean "or" like that in the OOP form
pure def myOr2(x, y) = x.or(y)
/// We can apply "or" to more than two arguments
pure def myOr3(x, y, z) = or(x, y, z)
/// When your expressions get bigger, you can stack them in `or { ... }`
pure def myOr4(x, y, z) = or {
x,
y,
z
}
```

Similar to "and", we can use the dot-notation, "or" over multiple arguments,
and the `or { ... }`

.

## 13. Boolean implication

*Progress:* 80%

**Code snippet:**

```
/// Boolean implication.
/// This operator is equivalent to `not(x).or(y)` as well as to `if (x) y else true`.
pure def myImplies(x, y) = x implies y
```

Perhaps, you remember Boolean implication from your math classes.
In some languages, it is written as `x -> y`

or `x => y`

.
In Quint is written as `x implies y`

, or, alternatively, `x.implies(y)`

.

If you don't like it, you don't have to use it:
`x implies y`

is equivalent to `not(x) or y`

.

Try the implication for all combinations of `false`

and `true`

:

`echo "false implies false" | quint`

`echo "false implies true" | quint`

`echo "true implies false" | quint`

`echo "true implies true" | quint`

## 14. Boolean equivalence

*Progress:* 86%

**Code snippet:**

```
/// Boolean equivalence.
/// It is equivalent to x == y, but this operator requires the arguments
/// to have the Boolean type.
pure def myIff(x, y) = x iff y
```

Finally, we have the equivalence operator `x iff y`

, or, alternatively, `x.iff(y)`

.
It is really like `x == y`

, but `x iff y`

does a bit more:
It requires `x`

and `y`

to be Booleans.

What is it is good for? If you know what protocol invariants are,
`x iff y`

looks nice when writing invariants and temporal formulas.
If you are not familiar with invariants and temporal formulas,
you probably do not need `iff`

yet.

Try `iff`

for all combinations of `false`

and `true`

:

`echo "false iff false" | quint`

`echo "false iff true" | quint`

`echo "true iff false" | quint`

`echo "true iff true" | quint`

## 15. Suming it up

*Progress:* 93%

We have covered all the operators over Booleans. If you want to see all operators in one place, check booleans.qnt (opens in a new tab).

We are experimenting with different kinds of tutorials. It would be great to learn, whether you liked this tutorial format, or not. Please vote in the discussion (opens in a new tab).

## The end

You have made it!