要请求 Lean 对一个表达式求值，请在编辑器中在它前面写上 #eval，编辑器随后会报告结果。 通常，通过将光标或鼠标指针悬停在 #eval 上即可看到结果。 例如，

3#eval 1 + 2

产生值

3

Lean 遵循算术运算符通常的优先级和结合性规则。也就是说，

11#eval 1 + 2 * 5

产生值 11，而不是 15。

虽然普通数学记法和大多数编程语言都使用圆括号（例如 f(x)）将函数应用于其参数，但 Lean 只是把函数写在其参数旁边（例如 f x）。 函数应用是最常见的操作之一，因此保持其简洁是值得的。 与其写成

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

要计算 "Hello, Lean!"，则应写作

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

其中，该函数的两个实参只是用空格写在它后面。

正如算术的运算顺序规则要求在表达式 (1 + 2) * 5 中使用括号一样，当函数的参数要通过另一次函数调用来计算时，也需要使用括号。 例如，在下面的表达式中需要括号

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

因为否则第二个 String.append 会被解释为第一个 String.append 的参数，而不是被传入 "oak " 和 "tree" 作为参数的函数。 必须先求出内部 String.append 调用的值，然后才能将其追加到 "great "，从而得到最终值 "great oak tree"。

命令式语言通常有两种条件构造：一种是条件语句，它根据一个 Boolean 值决定执行哪些指令；另一种是条件表达式，它根据一个 Boolean 值决定对两个表达式中的哪一个求值。 例如，在 C 和 C++ 中，条件语句使用 if 和 else 来书写，而条件表达式则使用三元运算符书写，其中 ? 和 : 将条件与分支分隔开。 在 Python 中，条件语句以 if 开始，而条件表达式将 if 置于中间。 由于 Lean 是一种面向表达式的函数式语言，因此没有条件语句，只有条件表达式。 它们使用 if、then 和 else 来书写。 例如，

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"。

为简洁起见，像这样的一系列求值步骤有时会用箭头写在它们之间：

could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
  String → String