Put a small file together

Put the pieces together in a small file: model data with a structure, define a transformation, evaluate a concrete input, and record a property as a named theorem. The definition says what the program does; the theorem states what callers may rely on.

The supplied Score type has a named points field. award returns a record update, preserving the shape of the value while changing that field. Your theorem works for any score whose points are known to be five, so it needs both a parameter and a hypothesis.

The new tactic is rw [h], short for rewrite. When h : s.points = 5, it replaces every s.points in the goal by 5, the same substitution you would do on paper. After unfolding award the goal mentions s.points + 3, and one rewrite turns it into a calculation that Lean finishes by itself.

You can keep your work with Download .lean below the editor. The downloaded file includes the definitions and exercise checks, so it can be opened as ordinary Lean code. When you want a local project, elan manages Lean versions, Lake builds the project, and the Lean 4 extension for VS Code displays goals as you edit. Start with the same Lean 4.30 toolchain used here.

Worked example

structure Account where
  balance : Nat

def credit (a : Account) (amount : Nat) : Account :=
  { a with balance := a.balance + amount }

theorem credit_known (a : Account) (h : a.balance = 10) : (credit a 2).balance = 12 := by
  unfold credit
  rw [h]

#eval (credit { balance := 4 } 3).balance

This miniature project updates a structure, proves a property under a hypothesis and evaluates a concrete call. Your exercise repeats that workflow with a score.