Review: build it without help
Define a type, a record and functions on them, and predict their output, with no step checklist.
In this course 11 / 11
No new material: each exercise mixes ideas from the whole course, without a checklist of steps. Hints only point in a direction; the full answer stays behind Reveal a solution.
Work the way you would on your own. Read the task, decide which kind of Lean you need (a def, a structure, an inductive, a pattern match, an if), write it, check it, and read the reply. If you are stuck, the lesson that introduced the idea is one click away in the course list.
Worked example
-- A reminder of the shapes, on a different type.
inductive Coin where
| heads
| tails
def turnOver : Coin → Coin
| .heads => .tails
| .tails => .heads
example : turnOver (turnOver .heads) = .heads := by
rfl
At the start of the proof on line 10. Everything above ⊢ may be used; the line below it is what must be proved.
An inductive type, a function by pattern matching, and a quick test. The exercises ask for each of these on other data.
You can model data, define functions on it and predict what they compute. The next course shows how to prove things about them.
Define an inductive type Light with constructors red, yellow and green. Define next : Light → Light so that red is followed by green, green by yellow and yellow by red. Define canGo : Light → Bool, which is true only for green.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
example : next Light.red = Light.green := by rfl example : next Light.green = Light.yellow := by rfl example : next Light.yellow = Light.red := by rfl example : canGo Light.green = true := by rfl example : canGo Light.red = false := by rfl example : canGo Light.yellow = false := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct