Basic Syntax

Autor

Modificat

11/04/2025

This chapter introduces the foundational elements of Lean 4’s syntax. We’ll learn how to define variables, write functions, and work with types and expressions, the essential building blocks of Lean 4 programming. By the end, we’ll be able to read and write basic Lean 4 programs, preparing us for more advanced topics ahead.

Let’s start with a fundamental question.

What is a type?

A type classifies data, defining what values it can hold and what operations can be performed on it. Types are essential in both programming and theorem proving, ensuring correctness and structuring reasoning. In Lean 4, types act as a safety mechanism:

A value of type Nat (natural number) can be 0, 1, 2, etc.
A value of type String can be "hello", "Lean 4", etc.
A function of type Nat → Nat takes a natural number as input and returns another natural number.

By assigning types to values and functions, Lean 4 prevents errors like adding a number to a string or applying a function to incompatible data.

Next, we’ll explore some fundamental Lean 4 commands.

Comment code

In Lean 4, comments help make code more readable and serve as documentation. They are ignored by the compiler and do not affect execution. Here’s how to write comments in Lean:

Single-line comments start with – and apply to the rest of the line.
Multi-line comments are enclosed between /- and -/.

comment.lean

-- This is a comment  

/-
This is a multi-line comment.
It can span multiple lines.
Useful for longer explanations. 
-/

check

We’ll begin with the #check command, a key tool for exploring Lean’s type system. The #check command allows us to inspect the type of an expression, definition, or theorem in Lean. It’s invaluable for understanding how Lean interprets our code and for troubleshooting type-related issues.

check.lean

#check true  
#check 42     
#check 'h'
#check ['h', 'e', 'l', 'l', 'o']
#check "hello"   
#check Nat

In these examples:

outputs Bool.true : Bool which tells us that true is of type Bool.
outputs 42 : Nat which tells us that 42 is of type Nat (natural number).
outputs "h" : Char which tells us that "h" is of type Char (a character).
outputs ['h', 'e', 'l', 'l', 'o'] : List Char which tells us that ['h', 'e', 'l', 'l', 'o'] is a list of characters.
outputs "hello" : String which tells us that "hello" is of type String.
outputs Nat : Type which tells us that Nat is of type Type.

print

The #print command allows us to inspect the definition of a function, theorem, or other named entity in Lean. It provides detailed information, including the type, implementation, and any dependencies. This command is especially useful for understanding how Lean’s standard library works or for debugging our own code.

print.lean

#print Bool 
#print Nat
#print Char
#print List
#print String
-- We cannot `#print Type` because this is a built-in concept
#print Type

In these examples:

#print Bool outputs

inductive Bool : Type
number of parameters: 0
constructors:
Bool.false : Bool
Bool.true : Bool

This tells us that Bool is an inductive type with no parameters and two constructors. Constructors are ways to provide elements of the given type—in this case, Bool.false represents the value false, and Bool.true represents the value true. Thus, an inductive type defines a new type by specifying a set of constructors that generate its elements. Each constructor may take arguments, including recursive references to the type itself. Inductive types are fundamental in Lean, serving as the basis for both data structures (such as natural numbers, lists, and trees) and logical propositions. We will explore inductive types in more detail later, but for now, understand that constructors define the possible values of a type, and Bool is a type with exactly two such values.

#print Nat outputs

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

As we can see, Nat is also an inductive type representing natural numbers, which do not require parameters. It has two constructors:

Nat.zero, which represents the number 0.
Nat.succ, which represents the successor of a natural number (essentially adding 1).

This definition allows natural numbers to be constructed starting from 0 and adding 1 repeatedly. Another way of denoting natural numbers in Lean is using ℕ. To type this symbol, you can use the shortcut \N.

#print Char outputs

structure Char : Type
number of parameters: 0
constructor:
Char.mk : (val : UInt32) → val.isValidChar → Char
fields:
val : UInt32
valid : self.val.isValidChar

Char is a structure representing a single character and does not have parameters. A structure in Lean is a way to define a type that groups together related data. The Char structure has a constructor called Char.mk, which takes:

A UInt32 value (a 32-bit unsigned integer) representing the Unicode code point of the character.
val.isValidChar, a proof that the value is a valid Unicode character.

Moreover, every element of type Char has two associated fields:

val: This field returns the Unicode value of the character.
valid: This field returns the proof that the code point is valid.

Thus, the Char structure combines the character value and its validity in a structured way. We will also explore structures in more detail in future chapters.

#print List outputs

inductive List.{u} : Type u → Type u
number of parameters: 1
constructors:
List.nil : {α : Type u} → List α
List.cons : {α : Type u} → α → List α → List α

List is an inductive type that represents a sequence of elements of a given type α. This type requires one parameter, α, where α is the type of elements in the list. The universe level u is used in the type definition to avoid paradoxes in type theory. For example, when we instantiate List with Nat, we get the type of lists of natural numbers (List Nat), and when instantiated with Char, we get the type of lists of characters (List Char). The List type has two constructors:

List.nil, which represents the empty list ([]).
List.cons, which adds an element to the front of a list.

Thus, List allows us to work with ordered sequences of elements, either empty or with elements added recursively.

#print String outputs

structure String : Type
number of parameters: 0
constructor:
String.mk : List Char → String
fields:
data : List Char

This indicates that String is a structure in Lean, with no parameters, that represents strings. The constructor for String is String.mk, which takes a List Char (a list of characters) as input and returns a String. Each element of type String has a field called data, which returns the list of characters that make up the string.

#print Type outputs an error because Type is a built-in concept in Lean’s logical foundation, not a user-defined term or definition. Type represents the universe of types in Lean, and querying it with #print is not valid because it is not something that can be printed in the same way as user-defined terms.

def

The def keyword is used to define a function or a value in Lean. It is one of the most fundamental constructs, allowing us to create reusable code—whether for simple values, functions, or more complex computations.

def.lean

-- Definition of number pi
def pi : Float := 3.1415926

Definitions can have parameters.

def.lean

-- Definition of the sum of two natural numbers
def sum (a b : Nat) : Nat := a + b

fun

The fun keyword is used to define anonymous functions (also called lambda functions) in Lean. These are functions that don’t have a name and are defined inline. The fun keyword is a core concept in functional programming. We can also use the λ (lambda) operator to define anonymous functions, which is written as \lambda in Lean.

fun.lean

-- Two anonymous ways of defining the sum of two natural numbers
#check fun (a b : Nat) => a + b
#check λ (a b : Nat) => a + b

The resulting type Nat → Nat → Nat represents a curried function, which is a fundamental concept in functional programming. This type can be understood as follows:

Nat → Nat → Nat is a function that takes a Nat (first argument) and returns another function.
The returned function then takes a Nat (second argument) and returns a Nat (final result).

This curried function type is equivalent to Nat → (Nat → Nat)—meaning a function that takes a Nat and returns a function from Nat to Nat. In Lean, function types are right-associative, so the parentheses are often omitted for clarity. Thus, Nat → Nat → Nat is interpreted as Nat → (Nat → Nat).

The function type

In general, if A and B are types, then A → B is a type representing all mappings from type A to type B. This means that any value of type A → B is a mapping that takes an element of type A and returns an element of type B. In Lean, we use \to to type the arrow → when writing this in code. We will explore this type in more detail later.

function.lean

-- The type of all mappings from Nat to Nat
#check Nat → Nat 
-- An example of an element of the above type
#check sum 3

This new construction provides an alternative approach to defining the previous sum mapping. The goal is to construct an element of type Nat → Nat → Nat. There are several ways to achieve this: either by using the fun keyword, as previously demonstrated, or by explicitly introducing the variables and specifying the expression that the mapping should return.

The latter approach uses the keywords by, intro, and exact. These are used in interactive proof mode, where you construct definitions step by step using tactics.

by: This keyword signals that the function definition will be built interactively using tactics.
intro: This tactic introduces the function’s arguments as hypotheses in the goal.
exact: This tactic is used to provide the exact value that satisfies the goal.

sum.lean

-- Two new ways of defining the sum of two natural numbers
def sum2 : Nat → Nat → Nat := fun a b => a + b
--
def sum3 : Nat → Nat → Nat := by
    intro a b 
    exact a + b

cases

The cases tactic splits the definition into two branches based on the value of the input. We will use it to define the Negation function for Booleans.

BoolNot.lean

def BoolNot : Bool → Bool := by
  intro b
  cases b
  -- b = false
  exact true
  -- b = true
  exact false

match

The match keyword is used for pattern matching. This is another way to handle different cases of the input.

BoolNot.lean

def BoolNot2 : Bool → Bool := by
  intro b
  match b with
    | false => exact true
    | true  => exact false

let

The let keyword is used to define local variables or terms within a proof or expression.

sphere.lean

def sphereVolume (r : Float) : Float :=
  let pi : Float := 3.1415926
  (4/3) * pi * r^3

eval

The #eval command is used to evaluate an expression and display its result. It is one of the most commonly used commands for testing and debugging code, as it allows us to see the output of a computation directly.

eval.lean

#eval sum 3 4
#eval (sum 3) 4
#eval (fun (a b : Nat) => a + b) 3 4
--
#eval pi
#eval Nat.succ 4 
#eval UInt32.isValidChar 104
#eval 'h'.val
#eval String.mk ['h', 'e', 'l', 'l', 'o']
#eval "hello".data

The first evaluations result in 7 because they compute the sum 3 + 4. After that, the following evaluations make use of previously defined values. For example, #eval pi returns the value of pi that was defined earlier. #eval Nat.succ 4 evaluates the successor function for natural numbers, applied to 4, returning 5 as the result. #eval UInt32.isValidChar 104 returns true, indicating that 104 is a valid Unicode character. #eval 'h'.val shows that the character 'h' has the Unicode value 104. Additionally, #eval String.mk ['h', 'e', 'l', 'l', 'o'] transforms the list of characters ['h', 'e', 'l', 'l', 'o'] into a string, in this case "hello". Finally, #eval "hello".data returns the list of characters that make up the string "hello", in this case ['h', 'e', 'l', 'l', 'o'].

variable

The keyword variable is used to declare variables that can be used later in the code. These variables are implicitly available in the context of any theorem, definition, or proof that follows. They allow us to introduce general assumptions or placeholders for types or values without needing to explicitly define them at each step.

variable.lean

variable (m n : Nat)
#check m

namespaces

Namespaces in Lean are used to organize code, helping with structure and readability. We can define variables, functions, or theorems within a namespace, and these definitions are scoped to that namespace, meaning they are only accessible inside it. When we exit a namespace, the variables defined inside it are no longer recognized. To access a variable defined within a namespace, we must reference it using the namespace name.

namespace.lean

namespace WorkSpace
-- Define a natural number `r` with the value 27
def r : Nat := 27
-- The variable `r` is perfectly defined within the namespace
#eval r   
end WorkSpace

-- Evaluating `r` outside the namespace will result in an error
#eval r  -- Error: unknown identifier 'r'

-- To access `r`, we must reference it using its namespace
#eval WorkSpace.r  -- Output: 27

open

The open keyword is used in Lean to bring definitions, theorems, or namespaces into the current scope, allowing us to reference them without needing to use their full qualified names. This helps make our code more concise and easier to read by reducing the need for repetitive namespace prefixes.

open.lean

open Workspace
#eval r