Basics

True to the title of this article series, we start from zero. Not “Hello, World!” but an actual zero: the natural number that forms the foundation of arithmetic.

Zero

-- From Zero to QED: let's start at the very beginning
def zero : Nat := 0

#eval zero  -- Output: 0

-- The natural numbers are defined inductively:
-- Nat.zero is the base case
-- Nat.succ n is the successor of n
def one : Nat := Nat.succ Nat.zero
def two : Nat := Nat.succ (Nat.succ Nat.zero)

#eval one   -- Output: 1
#eval two   -- Output: 2

-- Of course, we can just write the literals directly
def fortyTwo : Nat := 42

-- The answer to life, the universe, and everything
theorem deep_thought : fortyTwo = 6 * 7 := rfl

This first example introduces three toplevel declarations that you will use constantly:

• def defines a named value or function. Here def zero : Nat := 0 declares that zero has type Nat (natural number) and equals 0. Every Lean program is built from def declarations.

• #eval evaluates an expression and prints the result. This command runs code immediately, useful for testing as you work. Commands starting with # are interactive queries that do not create permanent definitions.

• theorem declares a proposition to be proved. The name deep_thought labels the statement fortyTwo = 6 * 7, and rfl (reflexivity) proves it by computation: both sides reduce to 42. Unlike def, theorem proofs are opaque and never unfold during type checking.

The natural numbers are perhaps the most fundamental type in mathematics and programming. Lean represents them inductively: zero is the base case, and every other natural number is the successor of another. This simple construction gives us the entire infinite sequence 0, 1, 2, 3, and so on.

Natural Numbers

Natural numbers in Lean represent non-negative integers, defined inductively just as Peano intended in 1889. They support standard arithmetic operations, but subtraction truncates at zero since negative results would fall outside the type. This has caused approximately as many bugs as unsigned integers in C, which is to say: more than anyone wants to admit.

-- Natural numbers (Nat) are non-negative integers: 0, 1, 2, 3, ...
def myNat : Nat := 42
def anotherNat : Nat := 100

-- Basic arithmetic
#eval 3 + 5      -- 8
#eval 10 - 3     -- 7 (truncated subtraction: 3 - 10 = 0)
#eval 4 * 7      -- 28
#eval 17 / 5     -- 3 (integer division)
#eval 17 % 5     -- 2 (modulo)

-- Natural number subtraction truncates at zero
#eval 3 - 10  -- 0, not -7

-- Comparison returns Bool
#eval 5 < 10     -- true
#eval 5 ≤ 5      -- true
#eval 10 == 10   -- true

Lean has two equality operators. The == operator is decidable equality, returning a Bool for use in programs. The = operator is propositional equality, returning a Prop for use in proofs. For runtime computation, use ==. For stating theorems, use =. Both work with #eval because Lean can decide equality for natural numbers.

Integers

When you need negative numbers, use Int. Integer arithmetic behaves as you would expect from standard mathematics, unburdened by the horrors of two’s complement overflow that have plagued systems programmers since the PDP-11.

-- Integers (Int) include negative numbers
def myInt : Int := -17
def posInt : Int := 42

-- Integer arithmetic handles negatives properly
-- Starting with a negative infers Int automatically
#eval -5 + 3     -- -2
#eval -4 * -3    -- 12
#eval -17 / 5    -- -3
#eval -17 % 5    -- -2
-- But positive minus larger needs annotation
#eval (3 : Int) - 10     -- -7

-- Converting between Nat and Int
#eval Int.ofNat 42             -- 42 as Int
#eval (42 : Int).toNat         -- 42 as Nat
#eval (-5 : Int).toNat         -- 0 (negative becomes 0)
#eval (42 : Int).natAbs        -- 42 (absolute value as Nat)
#eval (-42 : Int).natAbs       -- 42

Comments

Lean supports several comment styles. Single-line comments begin with -- and extend to the end of the line. Block comments are delimited by /- and -/ and can span multiple lines. Unlike C-style comments, Lean’s block comments nest properly, so you can comment out code that already contains comments.

Documentation comments are special. A comment starting with /-- attaches to the following declaration and is extracted by documentation tools. A comment starting with /-! provides module-level documentation, typically placed at the top of a file. Both support markdown formatting.

-- Single-line comments start with double dash
-- Everything after -- is ignored until end of line

/- Block comments are delimited by /- and -/
   They can span multiple lines
   and are useful for temporarily disabling code -/

/-- Documentation comments start with /-- and end with -/
    They attach to the following declaration and support markdown.
    Use these to document your API. -/
def documented (n : Nat) : Nat := n + 1

/-! Module-level documentation uses /-! and -/
    Place these at the top of a file to describe the module's purpose.
    Documentation tools extract these comments automatically. -/

-- Comments nest properly:
/- outer /- inner -/ still outer -/

-- The #check command is not affected by comments on the same line
#check Nat  -- this comment doesn't interfere

Modules and Namespaces

Lean organizes code into modules and namespaces. This section covers the practical syntax; we revisit the underlying mechanics in Type Theory.

Files and Modules. Each .lean file defines a module. The file Foo/Bar/Baz.lean defines module Foo.Bar.Baz. To use definitions from another module, import it at the top of your file with import Mathlib.Data.Nat.Prime or import Mathlib for an entire library. Imports are transitive: if A imports B and B imports C, then A has access to C’s definitions. The Lake build system (covered in Build System) manages dependencies and ensures modules are compiled in the correct order.

Namespaces. Namespaces group related definitions under a common prefix. They prevent name collisions and organize large codebases:

namespace Geometry2
  structure Point2 where
    x : Float
    y : Float

  def theOrigin : Point2 := ⟨0.0, 0.0⟩

  def dist (p q : Point2) : Float :=
    let dx := p.x - q.x
    let dy := p.y - q.y
    Float.sqrt (dx * dx + dy * dy)
end Geometry2

-- Access with full path
#eval Geometry2.dist Geometry2.theOrigin ⟨3.0, 4.0⟩  -- 5.0

The angle brackets ⟨ and ⟩ are shorthand for structure constructors. These two lines are equivalent:

def explicit : Point2 := Point2.mk 3.0 4.0
def shorthand : Point2 := ⟨3.0, 4.0⟩

The open command brings namespace contents into scope, so you can write dist instead of Geometry2.dist:

-- Open brings namespace contents into scope
open Geometry2 in
#eval dist theOrigin ⟨3.0, 4.0⟩  -- 5.0

-- Open for a definition
open Geometry2 in
def unitCirclePoint (θ : Float) : Point2 := ⟨Float.cos θ, Float.sin θ⟩

Sections and Variables. The section command creates a scope for temporary declarations. Variables declared with variable inside a section are automatically added as parameters to definitions that use them:

section VectorOps
  variable (α : Type) [Add α] [Mul α]

  -- α and the instances are automatically added as implicit parameters
  def doubleIt (x : α) : α := x + x
  def squareIt (x : α) : α := x * x
end VectorOps

#eval doubleIt Nat 21    -- 42
#eval squareIt Nat 7     -- 49

The bracket notation deserves explanation. Round brackets mark explicit arguments you pass directly. Square brackets mark instance arguments that Lean finds automatically through type class resolution. Here, [Add α] means the type must have an Add instance, which provides the + operator. Curly braces mark implicit arguments that Lean infers from context.

Scoping. Lean provides several mechanisms for limiting where names are visible. At the expression level, let bindings introduce local variables that exist only within the expression body. The where clause does the same but places definitions after their use, which some find more readable. Scopes nest, and inner bindings shadow outer ones with the same name.

-- let bindings create local scope within an expression
def hypotenuse (a b : Float) : Float :=
  let aSquared := a * a
  let bSquared := b * b
  Float.sqrt (aSquared + bSquared)
  -- aSquared and bSquared are not visible outside this def

-- where clauses provide the same scoping, but definitions come after use
def quadraticRoots (a b c : Float) : Float × Float :=
  ((-b + discriminant) / denom, (-b - discriminant) / denom)
where
  discriminant := Float.sqrt (b * b - 4 * a * c)
  denom := 2 * a

-- Scopes nest: inner let shadows outer
def shadowExample : Nat :=
  let x := 1
  let result :=
    let x := 2      -- shadows outer x
    x + 10          -- uses inner x: 12
  result + x        -- uses outer x: 12 + 1 = 13

#eval shadowExample  -- 13

At the declaration level, sections scope variable declarations (as shown above), namespaces scope definitions under a prefix, and private restricts visibility to the current file. The general principle: introduce names in the narrowest scope that makes sense. Local computations belong in let or where. Shared helpers belong in a namespace. Implementation details belong behind private.

Visibility. By default, all definitions are public. Mark definitions as private to hide them outside the current file:

namespace Internal
  private def helperVal : Nat := 42

  def publicApi : Nat := helperVal * 2
end Internal

#eval Internal.publicApi          -- 84
-- helperVal is not accessible outside this file

Export. The export command re-exports definitions from one namespace into another, making them available without opening the original:

namespace Math
  def square (x : Nat) : Nat := x * x
  def cube (x : Nat) : Nat := x * x * x
end Math

namespace Prelude
  -- Re-export square from Math into Prelude
  export Math (square)
end Prelude

-- Now square is available via Prelude without opening Math
#eval Prelude.square 5  -- 25

The Init Namespace. Every Lean file automatically imports the Init namespace, which provides foundational types and functions without explicit imports. This is Lean’s equivalent of Haskell’s Prelude or OCaml’s Stdlib, though the design differs.

Haskell’s Prelude is imported unqualified by default, meaning all its names are directly available. You disable this with NoImplicitPrelude. OCaml takes the opposite approach: all modules are available qualified (you write List.map), and you must explicitly open List to use names unqualified.

Lean splits the difference. The Init namespace is always available without qualification. Unlike Haskell, there is no pragma to disable it, but you can shadow any definition with your own. The Init hierarchy is organized into submodules (Init.Prelude, Init.Data, Init.Control), but from the user’s perspective it appears as a unified set of defaults.

Functions

Functions are first-class values in Lean. You can define them in multiple ways and partially apply them to create new functions.

def add (x : Nat) (y : Nat) : Nat :=
  x + y

def double : Nat → Nat :=
  fun x => 2 * x

def addFive := add 5  -- Partially applied function

#eval add 3 4        -- Output: 7
#eval double 21      -- Output: 42
#eval addFive 10     -- Output: 15

When declaring multiple parameters of the same type, you can group them: (x y z : Nat) is identical to (x : Nat) (y : Nat) (z : Nat). Use whichever reads better.

Pattern Matching

Pattern matching is a powerful feature for destructuring data and defining functions by cases.

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

def describe : Nat → String
  | 0 => "zero"
  | 1 => "one"
  | 2 => "two"
  | n => s!"many ({n})"

#eval factorial 5    -- Output: 120
#eval describe 0     -- Output: "zero"
#eval describe 100   -- Output: "many (100)"

The factorial definition uses n + 1 rather than the seemingly more natural | n => n * factorial (n - 1). This is not a style choice. Lean must verify that recursive calls terminate, and it does this by checking that arguments decrease structurally. The pattern n + 1 desugars to Nat.succ n, explicitly matching a successor. When you recurse on n, Lean sees that n is structurally smaller than Nat.succ n. With | n => ... factorial (n - 1), Lean cannot immediately see that n - 1 is smaller than n (subtraction is a function, not a constructor), so termination checking fails.

The describe function uses string interpolation with s!"many ({n})". The s! prefix enables interpolation: expressions inside {...} are evaluated and converted to strings. Without the prefix, curly braces are literal characters.

More Declarations

Abbreviations are transparent definitions that unfold automatically during elaboration. Use them for type aliases:

-- abbrev creates a transparent abbreviation (always unfolded)
abbrev NatPair := Nat × Nat
abbrev Predicate' (α : Type) := α → Bool

def isEvenPred : Predicate' Nat := fun n => n % 2 == 0
def sumPair (p : NatPair) : Nat := p.1 + p.2

#eval isEvenPred 4       -- true
#eval sumPair (3, 7)     -- 10

The interactive commands #check, #print, and #reduce help you explore code:

-- #check shows the type of an expression
#check (fun x : Nat => x + 1)  -- Nat → Nat
#check @List.map              -- shows full polymorphic type

-- #print shows information about a declaration
#print Nat.add
#print List

-- #reduce reduces an expression to normal form
#reduce (fun x => x + 1) 5    -- 6
#reduce List.map (· + 1) [1, 2, 3]  -- [2, 3, 4]

A complete reference of all declarations appears in the appendix. Advanced declarations like axiom, opaque, universe, notation, and set_option are covered in later articles where they arise naturally.

Function Composition

Lean provides three operators for combining functions:

Composition builds new functions by chaining existing ones. The ∘ operator reads right-to-left: in f ∘ g, apply g first, then f. Pipelines with |> read left-to-right, which often matches how you think about data transformations: “take this, then do that, then do this.”

def twice (n : Nat) := n * 2
def square (n : Nat) := n * n
def inc (n : Nat) := n + 1

-- ∘ composes right-to-left: (f ∘ g) x = f (g x)
#eval (square ∘ twice) 3           -- 36: square(twice(3)) = square(6)
#eval (twice ∘ square) 3           -- 18: twice(square(3)) = twice(9)
#eval (inc ∘ square ∘ twice) 3     -- 37: inc(square(twice(3)))

-- |> pipes left-to-right: x |> f |> g = g (f x)
#eval 3 |> twice |> square |> inc  -- 37: same computation, opposite order
#eval 10 |> twice                  -- 20
#eval [1, 2, 3] |> List.reverse    -- [3, 2, 1]

-- <| is low-precedence application: f <| x = f x
-- useful to avoid parentheses
#eval String.length <| "hello" ++ " world"  -- 11
#eval List.map twice <| [1, 2, 3]           -- [2, 4, 6]

-- chaining with methods vs pipes
#eval [1, 2, 3].map twice |> List.reverse        -- [6, 4, 2]
#eval ([1, 2, 3].map twice).reverse              -- same

-- composition builds new functions without naming arguments
def processThenSquare := square ∘ twice ∘ inc
#eval processThenSquare 2                        -- 36: square(twice(inc(2)))

The <| operator is just function application with low precedence. It lets you write f <| expensive computation instead of f (expensive computation). Some find this cleaner; others prefer explicit parentheses. Use whichever reads better.

Point-free style defines functions without naming their arguments: square ∘ twice rather than fun x => square (twice x). This can be elegant for simple compositions but obscure for complex ones. The goal is clarity, not cleverness.

Higher-Order Functions

Higher-order functions take functions as arguments. The classics: map transforms each element, filter keeps elements matching a predicate, foldl reduces a list to a single value by accumulating from the left.

And because Lean is also a theorem prover, we can prove properties by computation. The theorem add_comm_example states that 2 + 3 = 3 + 2, and rfl proves it because both sides reduce to 5. The examples at the end go further: reversing a list twice returns the original, list lengths add correctly, mapping a function produces the expected result.

What is the difference between #eval [1,2,3].reverse.reverse = [1,2,3] and example : [1,2,3].reverse.reverse = [1,2,3] := rfl? The #eval runs at runtime and prints true. The example is verified at compile time by the type checker, and if the equality did not hold, compilation would fail. Both check the same fact, but example catches the error before you ship. Note that this rfl proof verifies this specific list; proving it for all lists requires a theorem with induction. We cover proofs properly in Proofs.

-- Higher-order functions
#eval [1, 2, 3, 4, 5].map (· * 2)         -- [2, 4, 6, 8, 10]
#eval [1, 2, 3, 4, 5].filter (· > 2)      -- [3, 4, 5]
#eval [1, 2, 3, 4, 5].foldl (· + ·) 100   -- 115 (100 + 1 + 2 + 3 + 4 + 5)

-- Programs are proofs: addition is commutative
theorem add_comm_example : 2 + 3 = 3 + 2 := rfl

-- Computation IS proof: complex operations verified by evaluation
example : [1, 2, 3].reverse.reverse = [1, 2, 3] := rfl
example : [1, 2, 3].length + [4, 5].length = 5 := rfl
example : [1, 2, 3].map (· + 10) = [11, 12, 13] := rfl

From Values to Structure

For a complete reference of all toplevel declarations (def, theorem, inductive, structure, etc.) and interactive commands (#eval, #check, #print), see Appendix B.

You now have the building blocks: numbers, functions, modules, and the fundamental declarations. Next we cover the data structures that make programs useful: lists, arrays, maps, and user-defined types. After that, we explore control flow, polymorphism, effects, and IO. By the end of Arc I, you will have built a D&D character generator, which is either a useful demonstration of structured programming or an excuse to start a D&D campaign. Possibly both.