Write your own function
Parameters, a result type Lean holds you to, and checks that call your code.
In this course 6 / 11
Until now the definitions were given. Here is how to write one, with its parts labelled:
-- name parameters result body
def area (w h : Nat) : Nat := w * h
#eval area 3 412
Parameters go in brackets with their type. Two parameters of the same type can share brackets: (w h : Nat) means the same as (w : Nat) (h : Nat).
The result type is a promise, and Lean holds you to it. A body of the wrong type is rejected right at the definition:
def label (n : Nat) : String := nType mismatch
Under your answer are read-only checks that call your functions. They must compile, so your names, parameter types and results have to match what they expect.
Worked example
def area (w h : Nat) : Nat := w * h
def greet (name : String) : String := "Hello, " ++ name
#eval area 3 4
#eval greet "Ada"Your exercise has two definitions as well: one on numbers and one on text.
A definition has a name, typed parameters, a result type and a body. Lean checks the body against the result type.
- 1. Fizz Buzz Easy
Write triple, which multiplies a natural number by three, and shout, which adds ! to the end of 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