unfold (Lean)

Definition

unfold ( Lean)

The tactic unfold d expands occurrences of the definition d in the goal using its defining equations. It exposes what the definition means without performing the broader simplification of simp. Use unfold d at h to expand it in an assumption.

Example

Expanding a function definition

def addOne (n : ℕ) : ℕ := n + 1
 
example (n : ℕ) : addOne n = n + 1 := by
  unfold addOne
  rfl

unfold addOne changes the goal to n + 1 = n + 1. The tactic rfl proves this equality because both sides are definitionally equal.