Ask Lean about types
Read the type of a function, and tell data apart from claims.
In this course 4 / 11
Every expression in Lean has a type, and #check shows it as expression : type. Two definitions are given above the editor, double and greet. Ask about a function and Lean shows what it takes and what it returns:
#check greetgreet (name : String) : String
Give it its argument and what is left is a plain String. #check still does not run it; #eval would:
#check greet "Ada"
#eval greet "Ada"greet "Ada" : String "Hello, Ada"
Types have types too. Nat is a Type: it describes data. A claim such as 2 + 2 = 4 is a Prop: it describes something that may or may not be true. Keep that pair in mind; the proof courses build on it.
This is also the quickest way to understand a confusing error: #check each piece on its own and compare the answers.
Worked example
#check 42
#check "Lean"
#check true
#check Nat
#check 2 + 2 = 4#check true answers Bool.true : Bool: Lean prints the full name of the value. #check Nat answers Nat : Type, and the claim answers 2 + 2 = 4 : Prop.
Ask Lean instead of guessing. #check reports a type, #eval computes a value, Type describes data and Prop describes claims.
Ask Lean for the type of double, the type of double 3, and the type of the claim double 3 = 6.
Suggested steps
- Ask for the type of the function itself
- Ask for the type of the function applied to 3
- Ask for the type of the claim double 3 = 6
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:This exercise is judged by what Lean prints. Write the commands, press Check, then read the Output tab.
Knowledge check
Answer without looking back, then check your reasoning.
correct