lean2/doc/lean/expr.md

Expressions

Lean is based on dependent type theory, and is very similar to the one used in the Boole and Coq systems. In contrast to Coq, Lean is classical.

In Lean, we have the following kind of expressions: constants, ,function applications, (heterogeneous) equality, local variables, lambdas, dependent function spaces (aka Pis), let expressions, and Types.

Constants

Constants are essentially references to variable declarations, definitions, axioms and theorems in the environment. In the following example, we use the command variables to declare x and y as integers. The check command displays the type of the given expression. The x and y in the check command are constants. They reference the objects declared using the command variables.

variables x y : Nat
check x + y

In the following example, we define the constant s as the sum of x and y using the definition command. The eval command evaluates (normalizes) the expression s + 1. In this example, eval will just expand the definition of s, and return x + y + 1.

definition s := x + y
eval s + 1

Function applications

In Lean, the expression f t is a function application, where f is a function that is applied to t. In the following example, we define the function max. The eval command evaluates the application double 3, and returns the value 6.

import tactic    -- load basic tactics such as 'simp'
definition double (x : Nat) : Nat := x + x
eval double 3

In the following command, we define the function inc, and evaluate some expressions using inc and max.

definition inc (x : Nat) : Nat := x + 1
eval inc (inc (inc 2))
eval double (inc 3)