Evaluate and inspect
Run a calculation with #eval and ask for its type with #check.
In this course 2 / 11
Two commands let you ask Lean questions without writing a claim. #eval runs an expression and shows the result:
#eval 3 * 412
#check does not run anything. It tells you what type of thing the expression is:
#check 3 * 43 * 4 : Nat
Nat is Lean's type of natural numbers: 0, 1, 2 and so on. So the two commands answer two different questions: #eval answers “what does this produce?”, #check answers “what kind of thing is this?”. Write one command per line; the answers appear in the Output tab.
Neither command proves anything. A printed 12 is a result for this one input. The claims of the previous lesson were checked by Lean as proofs.
Worked example
#eval 3 * 4
#check 3 * 4
#eval "Hello, " ++ "Lean"
#check "Lean"++ joins two texts, and the type of a text is String.
#eval computes a value. #check reports a type. Neither one proves a claim.
Evaluate (3 + 4) * 2, then ask Lean for the type of the same expression.
Suggested steps
- Evaluate the expression with #eval
- Ask for its type with #check
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