{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProgrammingBasics.Operators where

Operators#

Let us begin by importing the definitions from the previous module:

open import Padova2025.ProgrammingBasics.Booleans

The import keyword causes the respective module to be loaded; by open, all its definitions are brought into scope. Without open, we would need to use Padova2025.ProgrammingBasics.Booleans.Bool to refer to the type of Booleans.

Example: Logical AND#

The logical AND operator could be defined in Agda as follows, specifying one clause for each of the four possible cases.

and : Bool → Bool → Bool
and false false = false
and false true  = false
and true  false = false
and true  true  = true

From blackboard mathematics, we might have expected the type signature to read and : Bool × Bool → Bool. For now, let us not worry about this issue and just accept the displayed syntax as Agda’s way of introducing functions with two parameters. We will later meet a satisfying explanation.

Here is how the operator could be used:

example-usage : Bool
example-usage = and false (and true false)

This piece of code looks a bit like Lisp. We can mimic blackboard notation more closely by renaming the function _&&_. Semantically, nothing changes; syntactically, the underscores indicate that the _&&_ function should be used as an infix operator with the arguments supplied to the left and the right.

infixr 6 _&&_
_&&_ : Bool → Bool → Bool
false && false = false
false && true  = false
true  && false = false
true  && true  = true

The first line in this snippet, infixr 6 _&&_, is optional and only included to tell Agda how tightly our new operator should bind. For instance, later we will provide _+_ with precedence level 6 and _*_ with precedence level 7, so that expressions like a + b * c are correctly parsed as a + (b * c) instead of the incorrect (a + b) * c.

We can then rewrite example-usage as follows.

example-usage' : Bool
example-usage' = false && (true && false)

Exercise: Logical OR#

In a similar vein, implement the logical OR operator.

Exercise 1_||_

infixr 5 _||_
_||_ : Bool → Bool → Bool
false || y = {!!}
true  || y = {!!}

Your solution

Reference solution

infixr 5 _||_
_||_ : Bool → Bool → Bool
false || y = y
true  || y = true

Exercise: A better definition of logical AND#

The definition of _&&_ offered above is needlessly complex. Instead of four defining clauses, we can make do with two. Find this shorter alternative definition.

Exercise 2_&&'_

_&&'_ : Bool → Bool → Bool
_&&'_ = {!!}

The reference solution uses: false true

Your solution

Reference solution

_&&'_ : Bool → Bool → Bool
_&&'_ false y = false
_&&'_ true  y = y

As a rule of thumb, function definitions which make do with fewer case distinctions are better, because such definitions allow us to give shorter proofs, as Agda is able to simplify terms to a larger extent. For instance, while it is true that false && y is false for every value of y, this fact is not evident to Agda and instead needs to be proven. For _&&'_, in contrast, this identity is manifest.