Define data by constructors
Create a three-state type and write an exhaustive transition function.
In this course 9 / 13
A structure describes one shape with several fields. An inductive type describes several possible shapes. inductive Mode creates a type whose only values are the constructors you list.
A function over an inductive type can pattern-match on those constructors. Each equation says what to return for one possible input. Lean checks exhaustiveness, so leaving out a constructor is an error rather than a forgotten runtime case.
Constructor names are qualified by the type, such as Mode.off. Inside a match or equation block, the shorter .off is enough when Lean already knows that a Mode is expected.
Your function forms a cycle. This is a small state machine: every input has one intentional successor, and the type prevents callers from inventing a fourth state.
Worked example
inductive Door where
| open
| closed
def toggle : Door → Door
| .open => .closed
| .closed => .open
#check toggle Door.openBoth constructors are handled explicitly. Your exercise has three constructors, so the function needs three equations.
An inductive type lists every valid shape. Pattern matching handles those shapes explicitly, and Lean checks that none is forgotten.
Define an inductive type Mode with constructors off, warm and bright. Define advance so they cycle in that order.
Suggested steps
- Declare all three
Modeconstructors - Give
advancethe typeMode → Mode - Write one equation for every constructor
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\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 : advance Mode.off = Mode.warm := by rfl example : advance Mode.warm = Mode.bright := by rfl example : advance Mode.bright = Mode.off := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct