1.4 Basic Syntax and Expressions

Lean code is built from expressions. An expression may be a value, a function, a type, a proposition, or a proof. The same syntactic system is used for computation and reasoning, so learning the basic expression language is the first step toward writing both programs and theorems.

Problem

You want to read and write small Lean expressions, understand their types, and recognize how Lean parses ordinary definitions and proof terms.

Solution

Use #check to inspect the type of an expression and #eval to compute expressions that have executable content.

#check 5
#check Nat
#check String
#check true
#check fun x : Nat => x + 1

#eval 5 + 7
#eval "Lean" ++ " " ++ "Cookbook"
#eval (fun x : Nat => x + 1) 10

Typical output includes types such as:

5 : Nat
Nat : Type
String : Type
true : Bool
fun x => x + 1 : Nat -> Nat
12
"Lean Cookbook"
11

The command #check asks Lean to infer a type. The command #eval asks Lean to compute a value.

Expressions

An expression is any Lean term that can be checked by the type system.

Examples:

42
"hello"
true
Nat
Nat -> Nat
fun x : Nat => x + 1

Each expression has a type.

#check 42              -- 42 : Nat
#check "hello"         -- "hello" : String
#check true            -- true : Bool
#check Nat             -- Nat : Type
#check Nat -> Nat      -- Nat -> Nat : Type

Types themselves are expressions. For example, Nat has type Type.

Function Application

Function application is written by placing the argument after the function.

#eval Nat.succ 4

The result is:

Multiple arguments are written by placing them in sequence:

#eval Nat.add 3 4

This means:

(Nat.add 3) 4

Function application associates to the left. Therefore:

f x y z

means:

(((f x) y) z)

Function Types

The type:

Nat -> Nat

means a function from natural numbers to natural numbers.

A function with two arguments has a curried type:

Nat -> Nat -> Nat

This means:

Nat -> (Nat -> Nat)

A function takes one argument and returns another function. This convention makes partial application natural.

def addThree : Nat -> Nat -> Nat :=
  fun x y => x + y + 3

#check addThree
#check addThree 4
#eval addThree 4 5

The expression addThree 4 is itself a function.

Lambda Expressions

A lambda expression creates an anonymous function.

fun x : Nat => x + 1

This expression has type:

Nat -> Nat

Several arguments can be written together:

fun x y : Nat => x + y

This is shorthand for:

fun x : Nat => fun y : Nat => x + y

Lambda expressions are useful when a small function is needed only once.

#eval List.map (fun x : Nat => x + 1) [1, 2, 3]

Expected result:

[2, 3, 4]

Let Expressions

A let expression gives a local name to a value.

#eval
  let x := 10
  let y := 20
  x + y

Expected result:

A let expression is still an expression. It computes by replacing the local name with its value.

You can also annotate the type:

#eval
  let x : Nat := 10
  x + 5

Annotations are useful when Lean cannot infer the intended type.

Parentheses

Parentheses control parsing.

#eval (fun x : Nat => x + 1) 5

Without parentheses, Lean would try to parse the expression differently.

Parentheses are also useful in nested applications:

#eval Nat.succ (Nat.succ 3)

Expected result:

Infix Operators

Many functions have infix notation.

#eval 2 + 3
#eval 10 - 4
#eval 3 * 5

These are notation for ordinary functions. For example:

2 + 3

is notation for addition on natural numbers.

Precedence determines how expressions are grouped.

#eval 2 + 3 * 4
#eval (2 + 3) * 4

Expected results:

14
20

Type Ascription

A type ascription tells Lean the intended type of an expression.

#check (5 : Nat)
#check ("hello" : String)

This is useful when literals are overloaded.

#check (0 : Nat)
#check (0 : Int)

The same printed literal may be elaborated at different types, depending on context.

Propositions as Expressions

Propositions are also expressions.

#check True
#check False
#check 1 = 1
#check Nat

Typical output:

True : Prop
False : Prop
1 = 1 : Prop
Nat : Type

A proof is an expression whose type is a proposition.

#check True.intro
#check rfl

The term True.intro proves True. The term rfl proves equalities that hold by reflexivity or definitional computation.

Definitions

A definition binds a name to an expression.

def one : Nat :=
  1

def two : Nat :=
  one + one

After these declarations, the names can be checked and evaluated.

#check one
#eval two

Expected result:

The general shape is:

def name : Type :=
  expression

Lean checks that expression has the declared type.

Theorems as Expressions

A theorem binds a name to a proof expression.

theorem true_example : True :=
  True.intro

The general shape is:

theorem name : proposition :=
  proof

A theorem is checked like any other declaration. The difference is that its declared type lies in Prop.

A tactic proof produces the same kind of proof term:

theorem implication_example (P : Prop) : P -> P := by
  intro h
  exact h

This theorem says that every proposition implies itself.

Holes

A hole asks Lean to report what it needs at that point.

def addOne (n : Nat) : Nat :=
  _

Lean reports that the hole has expected type Nat.

Holes are useful during development because they reveal the local context and the target type.

A named hole can appear more than once:

def pairSame (n : Nat) : Nat × Nat :=
  (?x, ?x)

Lean reports a goal named ?x.

Commands vs Expressions

Some Lean syntax is a command, not an expression.

Commands include:

def
theorem
#check
#eval
import
namespace
end

Expressions include:

5
Nat
fun x : Nat => x + 1
x + y
True

Commands modify or inspect the environment. Expressions are the terms that Lean checks.

Recipe: Inspect Before You Prove

When a proof or definition fails, inspect smaller pieces.

#check Nat.succ
#check Nat.succ 3
#eval Nat.succ 3

Then build the final declaration:

def next (n : Nat) : Nat :=
  Nat.succ n

This style avoids guessing. Lean becomes easier to use when each subexpression has a known type.

Common Pitfalls

If Lean reports a type mismatch, insert a type ascription to make the intended type explicit.

If function application parses incorrectly, add parentheses.

If a literal has the wrong type, annotate it.

If a name is unknown, check imports and namespaces.

If a theorem looks like a definition, remember that the difference is its type: propositions live in Prop.

Takeaway

Lean programs and proofs are built from expressions. Every expression has a type, and types themselves are expressions. Function application, lambda abstraction, let binding, type ascription, and proposition formation are the basic forms you need before definitions, theorems, tactics, and larger modules become predictable.