lean-fp-basics

name	lean-fp-basics
description	Lean 4 fundamentals including syntax, structures, inductive types, and polymorphism. Use when writing basic Lean code, defining custom data types, pattern matching, or learning core language patterns.
allowed-tools	Read, Grep, Glob

Lean 4 Functional Programming Basics

Lean 4 fundamentals: syntax, structures, inductive types, and polymorphism. Use when writing basic Lean code, defining custom data types, or learning core language patterns.

Trigger terms: "lean syntax", "define type", "structure", "inductive", "pattern matching", "polymorphism", "Lean basics"

---

Function Definition

def add1 (n : Nat) : Nat := n + 1

def maximum (n k : Nat) : Nat :=
  if n < k then k else n

Commands: #check (show type), #eval (evaluate), #print (show definition)

---

Structures (Product Types)

structure Point where
  x : Float
  y : Float
  deriving Repr

def origin : Point := { x := 0.0, y := 0.0 }

-- Update syntax (functional update)
def zeroX (p : Point) : Point := { p with x := 0 }

When to use: Fixed collection of named fields, all fields always present, want .field accessor syntax.

---

Inductive Types (Sum Types)

inductive Sign where
  | pos | neg | zero

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

Pattern Matching:

def isZero : Nat → Bool
  | .zero => true
  | .succ _ => false

When to use: Multiple constructors, different shapes, recursive data, need pattern matching.

---

Decision: Structure vs Inductive

Does your type need:
├─ Multiple constructors? → inductive
├─ Recursive definition? → inductive
├─ Different shapes per variant? → inductive
└─ Fixed fields always present? → structure

---

Polymorphism

-- Explicit type parameter
def replaceX (α : Type) (p : PPoint α) (x : α) : PPoint α := { p with x }

-- Implicit (preferred) - compiler infers
def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | _ :: ys => 1 + length ys

-- Provide implicit explicitly when needed
#check ([] : List Int)
#check List.length (α := Int)

Use implicit {α}: When type is inferrable from arguments. Use explicit (α): When type only in return, or empty containers.

---

Common Mistakes

Forgetting pattern exhaustiveness:

-- ❌ Missing case
def f : Option Nat → Nat
  | some n => n

-- ✓ Handle all cases
def f : Option Nat → Nat
  | some n => n
  | none => 0

Structures aren't mutable:

-- ❌ Won't compile
p.x := 5

-- ✓ Create new with update
{ p with x := 5 }

---

See Also

• lean-fp-type-classes - Overloading with type classes
• lean-fp-monads - Effect handling
• lean-tp-foundations - Type theory background

Source: Functional Programming in Lean