Module 1 · Lesson 5

Syntax & Notation

Learn how Lean notation maps to function calls, how to read infix operators, and how to use Unicode symbols without confusion. Lean's syntax is designed for readability—once you understand the patterns, code becomes self-documenting.

Infix Operators are Functions

Most operators in Lean are just functions written in infix form. The +in 2 + 3 is actually calling a function. You can always use prefix notation if it helps understanding:

lean

1-- Infix form (what you normally write)
2#eval 2 + 3     -- 5
3
4-- Prefix form (same thing!)
5#eval HAdd.hAdd 2 3  -- 5
6
7-- This works for all operators
8#eval 10 - 3         -- 7
9#eval HSub.hSub 10 3 -- 7
10
11-- Comparison operators too
12#eval 5 > 3          -- true
13#eval GT.gt 5 3      -- true
14
15-- You can use parentheses to make precedence explicit
16#check (2 + 3) * 4   -- Nat

Key Takeaway

If you're ever unsure what an operator does, you can look up its prefix form using #check. This reveals the underlying function.

Unicode and ASCII Equivalents

Lean supports Unicode symbols for clarity, making code look more like mathematical notation. Most have ASCII alternatives, so you can choose whichever feels more comfortable:

lean

1-- Function arrows
2#check Nat → Nat       -- Unicode arrow (\to)
3#check Nat -> Nat      -- ASCII arrow
4
5-- Universal quantifier
6#check ∀ n : Nat, n = n   -- Unicode (\forall)
7#check forall n : Nat, n = n
8
9-- Existential quantifier
10#check ∃ n : Nat, n > 0   -- Unicode (\exists)
11#check Exists fun n => n > 0
12
13-- Product types
14#check α × β           -- Unicode (\times)
15#check Prod α β        -- Prefix form
16
17-- Lambda
18#check λ x => x + 1    -- Unicode (\l)
19#check fun x => x + 1  -- ASCII
20
21-- Common symbols
22-- ∧ = and  (\and)    ∨ = or   (\or)
23-- ¬ = not  (\neg)    ≠ = ne   (\ne)
24-- ≤ = le   (\le)     ≥ = ge   (\ge)

💡

In VS Code, type \\forall, \\to, or \\alpha to insert Unicode symbols quickly. You can also hover over a Unicode symbol to see its input sequence.

Dot Notation

Dot notation is shorthand for passing the left side as the first argument. It makes code read more naturally, especially for chained operations:

lean

1-- These are equivalent:
2#check List.length [1, 2, 3]
3#check [1, 2, 3].length        -- Dot notation ✓
4
5#check List.map (fun x => x * 2) [1, 2, 3]
6#check [1, 2, 3].map (fun x => x * 2)  -- Cleaner ✓
7
8-- Chaining operations
9#eval [1, 2, 3, 4, 5]
10  .filter (· > 2)    -- [3, 4, 5]
11  .map (· * 10)      -- [30, 40, 50]
12  .reverse           -- [50, 40, 30]
13
14-- String operations
15#eval "Hello World".toUpper.drop 6  -- "WORLD"
16
17-- Works with nested types too
18#eval (some [1, 2, 3]).map List.length  -- some 3

The · (Dot) Placeholder

The centered dot · creates a short lambda. It stands for "the argument goes here."

lean

1-- These are equivalent:
2#eval [1, 2, 3].map (· + 1)          -- [2, 3, 4]
3#eval [1, 2, 3].map (fun x => x + 1) -- [2, 3, 4]
4
5-- More examples
6#eval [1, 2, 3].filter (· > 1)       -- [2, 3]
7#eval [1, 2, 3].map (· * ·)          -- Error! Only one · allowed
8
9-- Use for comparison
10#eval [2, 1, 3].mergeSort (· < ·)    -- Error! Can't use two dots
11#eval [2, 1, 3].mergeSort (fun a b => a < b)  -- [1, 2, 3]

ℹ

The · placeholder works best for simple expressions. For complex lambdas with multiple arguments, use fun.

Common Mistakes

Mistake 1: Using = instead of :=

lean

1-- ❌ Wrong: = is for equations/proofs
2-- def x = 5  
3
4-- ✓ Correct: := is for definitions
5def x := 5
6
7-- = is used in propositions
8example : 2 + 2 = 4 := rfl

Mistake 2: Confusing -> and =>

lean

1-- -> (or →) is for function TYPES
2#check Nat -> Nat     -- A function type
3#check Nat → Nat      -- Same thing
4
5-- => is for lambda BODIES and match arms
6#check fun x => x + 1 -- A lambda expression
7example : Nat -> Nat := fun x => x * 2
8
9-- In match expressions
10def describe (n : Nat) : String :=
11  match n with
12  | 0 => "zero"       -- => in match arms
13  | _ => "positive"

Mistake 3: Precedence surprises

lean

1-- Function application has high precedence
2#check List.map (· + 1) [1, 2, 3]  -- ✓
3-- #check List.map · + 1 [1, 2, 3] -- ❌ Confusing
4
5-- Be explicit when chaining
6#eval (1 + 2) * 3     -- 9
7#eval 1 + 2 * 3       -- 7 (multiplication first)
8
9-- Logical operators
10#check true && false || true   -- (true && false) || true
11#check true && (false || true) -- Explicit is clearer

Precedence & Parentheses

Lean follows standard mathematical precedence, but when in doubt, add parentheses. This is especially useful when learning new operators.

lean

1#check 2 + 3 * 4      -- parsed as 2 + (3 * 4)
2#check (2 + 3) * 4    -- explicit grouping
3
4#check 1 + 2 + 3      -- left associative: (1 + 2) + 3
5#check 2 ^ 3 ^ 2      -- right associative: 2 ^ (3 ^ 2) = 512
6
7-- Function application is left-associative
8#check f x y z        -- ((f x) y) z
9
10-- Type arrows are right-associative
11#check Nat → Nat → Nat  -- Nat → (Nat → Nat)

Named Arguments

Named arguments make code more readable and let you pass arguments in any order:

lean

1def greet (name : String) (formal : Bool := false) : String :=
2  if formal then s!"Good day, {name}." else s!"Hey {name}!"
3
4-- Positional
5#eval greet "Alice" true
6
7-- Named (order doesn't matter!)
8#eval greet (formal := true) (name := "Bob")
9
10-- Especially useful with many similar arguments
11def createUser (name : String) (email : String) (age : Nat) := 
12  s!"{name} ({email}), age {age}"
13
14#eval createUser 
15  (name := "Alice") 
16  (email := "[email protected]") 
17  (age := 30)

Pipeline Operators

Pipeline operators help with readable data transformations:

lean

1-- Forward pipe: passes result to next function
2#eval [1, 2, 3] |> List.reverse |> List.length  -- 3
3
4-- Equivalent to:
5#eval List.length (List.reverse [1, 2, 3])  -- 3
6
7-- Chained example
8def process (xs : List Nat) : Nat :=
9  xs 
10    |> List.filter (· > 0)
11    |> List.map (· * 2)
12    |> List.sum
13
14#eval process [0, 1, 2, 3]  -- 12

Exercise 1: Translate Notation

Rewrite the following expression using prefix notation and verify that Lean accepts it:

lean

1-- Infix form
2#eval (2 + 3) * 4  -- 20
3
4-- Prefix form
5#eval HMul.hMul (HAdd.hAdd 2 3) 4  -- 20

Exercise 2: Dot Notation

Rewrite using dot notation and chain the operations:

lean

1-- Before
2#eval List.length (List.reverse [1, 2, 3])
3
4-- After (with dot notation)
5#eval [1, 2, 3].reverse.length  -- 3

Exercise 3: Placeholder Dot

Use · to simplify these lambdas:

lean

1-- Before
2#eval [1, 2, 3].map (fun x => x * 2)
3#eval [1, 2, 3].filter (fun x => x > 1)
4
5-- After
6#eval [1, 2, 3].map (· * 2)     -- [2, 4, 6]
7#eval [1, 2, 3].filter (· > 1)  -- [2, 3]

Key Takeaway

If syntax feels mysterious, rewrite it using explicit function calls. Lean's notation is designed for readability, not magic.

Local Scope Next: Structures