# Evaluating Expressions

The most important thing to understand as a programmer learning Lean
is how evaluation works. Evaluation is the process of finding the
value of an expression, just as one does in arithmetic. For instance,
the value of 15 - 6 is 9 and the value of 2 × (3 + 1) is 8.
To find the value of the latter expression, 3 + 1 is first replaced by 4, yielding 2 × 4, which itself can be reduced to 8.
Sometimes, mathematical expressions contain variables: the value of *x* + 1 cannot be computed until we know what the value of *x* is.
In Lean, programs are first and foremost expressions, and the primary way to think about computation is as evaluating expressions to find their values.

Most programming languages are *imperative*, where a program consists
of a series of statements that should be carried out in order to find
the program's result. Programs have access to mutable memory, so the
value referred to by a variable can change over time. In addition to mutable state, programs may have other side
effects, such as deleting files, making outgoing network connections,
throwing or catching exceptions, and reading data from a
database. "Side effects" is essentially a catch-all term for
describing things that may happen in a program that don't follow the
model of evaluating mathematical expressions.

In Lean, however, programs work the same way as mathematical
expressions. Once given a value, variables cannot be reassigned. Evaluating an expression cannot have side effects. If two
expressions have the same value, then replacing one with the other
will not cause the program to compute a different result. This does
not mean that Lean cannot be used to write `Hello, world!`

to the
console, but performing I/O is not a core part of the experience of
using Lean in the same way. Thus, this chapter focuses on how to
evaluate expressions interactively with Lean, while the next chapter
describes how to write, compile, and run the `Hello, world!`

program.

To ask Lean to evaluate an expression, write `#eval`

before it in your
editor, which will then report the result back. Typically, the result
is found by putting the cursor or mouse pointer over `#eval`

. For
instance,

```
#eval 1 + 2
```

yields the value `3`

.

Lean obeys the ordinary rules of precedence and associativity for arithmetic operators. That is,

```
#eval 1 + 2 * 5
```

yields the value `11`

rather than
`15`

.

While both ordinary mathematical notation and the majority of
programming languages use parentheses (e.g. `f(x)`

) to apply a function to its
arguments, Lean simply writes the function next to its
arguments (e.g. `f x`

). Function application is one of the most common operations,
so it pays to keep it concise. Rather than writing

```
#eval String.append("Hello, ", "Lean!")
```

to compute `"Hello, Lean!"`

,
one would instead write

```
#eval String.append "Hello, " "Lean!"
```

where the function's two arguments are simply written next to it with spaces.

Just as the order-of-operations rules for arithmetic demand
parentheses in the expression `(1 + 2) * 5`

, parentheses are also
necessary when a function's argument is to be computed via another
function call. For instance, parentheses are required in

```
#eval String.append "great " (String.append "oak " "tree")
```

because otherwise the second `String.append`

would be interpreted as
an argument to the first, rather than as a function being passed
`"oak "`

and `"tree"`

as arguments. The value of the inner `String.append`

call must be found first, after which it can be appended to `"great "`

,
yielding the final value `"great oak tree"`

.

Imperative languages often have two kinds of conditional: a
conditional *statement* that determines which instructions to carry
out based on a Boolean value, and a conditional *expression* that
determines which of two expressions to evaluate based on a Boolean
value. For instance, in C and C++, the conditional statement is
written using `if`

and `else`

, while the conditional expression is
written with a ternary operator `?`

and `:`

. In Python, the
conditional statement begins with `if`

, while the conditional
expression puts `if`

in the middle.
Because Lean is an expression-oriented functional language, there are no conditional statements, only conditional expressions.
They are written using `if`

, `then`

, and `else`

. For
instance,

```
String.append "it is " (if 1 > 2 then "yes" else "no")
```

evaluates to

```
String.append "it is " (if false then "yes" else "no")
```

which evaluates to

```
String.append "it is " "no"
```

which finally evaluates to `"it is no"`

.

For the sake of brevity, a series of evaluation steps like this will sometimes be written with arrows between them:

```
String.append "it is " (if 1 > 2 then "yes" else "no")
===>
String.append "it is " (if false then "yes" else "no")
===>
String.append "it is " "no"
===>
"it is no"
```

## Messages You May Meet

Asking Lean to evaluate a function application that is missing an argument will lead to an error message. In particular, the example

```
#eval String.append "it is "
```

yields a quite long error message:

```
expression
String.append "it is "
has type
String → String
but instance
Lean.MetaEval (String → String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
```

This message occurs because Lean functions that are applied to only some of their arguments return new functions that are waiting for the rest of the arguments. Lean cannot display functions to users, and thus returns an error when asked to do so.

## Exercises

What are the values of the following expressions? Work them out by hand, then enter them into Lean to check your work.

`42 + 19`

`String.append "A" (String.append "B" "C")`

`String.append (String.append "A" "B") "C"`

`if 3 == 3 then 5 else 7`

`if 3 == 4 then "equal" else "not equal"`