Write your own function
Parameters, a result type Lean holds you to, and checks that call your code.
In this course 6 / 10
Up to now the definitions were handed to you. Writing one has four parts, in this order: the keyword def, the name, the parameters with their types in brackets, and after a colon the result type, then := and the body.
Parameters of the same type share one pair of brackets. def area (w h : Nat) : Nat takes two natural numbers, and writing (w : Nat) (h : Nat) would mean exactly the same thing.
The result type is not documentation. Lean checks the body against it and rejects the definition on the spot if they disagree, naming the type it found and the type you promised. That error arrives at the definition, long before anything tries to use it.
Below your answer are examples that call what you wrote. They are read-only and they have to compile, so your names, your parameter types and your results all have to line up with them. That is the same contract a real codebase has with its tests.
Worked example
-- name parameters result type body
def area (w h : Nat) : Nat := w * h
#eval area 3 4 -- 12
#check area -- area (w h : Nat) : Nat
-- The body is checked against the result type you promised:
-- def area’ (w h : Nat) : String := w * h
--
-- Type mismatch
-- w * h
-- has type
-- Nat
-- but is expected to have type
-- StringOne definition over two numbers, with its parts lined up above it. Your exercise wants two definitions, and the second one works on String rather than Nat — so its parameter type, its result type and the operator in its body all change together.
A definition names its parameters and promises a result type, and Lean holds the body to that promise.
Write two definitions: triple, which multiplies a natural number by three, and shout, which appends an exclamation mark to a string.
Suggested steps
- Define triple, from a Nat to a Nat
- Define shout, from a String to a String
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.
-- These run under your definitions and have to compile. example : triple 4 = 12 := by rfl example : triple 0 = 0 := by rfl example : shout "go" = "go!" := by rfl example : shout "" = "!" := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct