Evaluate and inspect
Run a calculation with #eval and inspect its type with #check.
In this course 2 / 14
#eval asks Lean to run a calculation and print its answer. For example, #eval 3 * 4 prints 12. You do not need a theorem to try a calculation.
#check asks for a type. #check (3 * 4) reports that the expression has type Nat: it is a natural number. It does not print the result of the multiplication.
These commands answer different questions. Use #eval for “what value does this produce?” and #check for “what kind of expression is this?”. Put each command on its own line.
A printed result is not a proof of a claim. The theorem in the first lesson asked Lean to check evidence for an equality. Here you are exploring expressions; the Output tab shows their answers.
Worked example
#eval 3 * 4
#check (3 * 4)
#eval "Hello, " ++ "Lean"The first line prints 12. The second reports a Nat. The last joins two strings and prints "Hello, Lean".
Use #eval to compute and #check to inspect a type. Neither command proves a theorem.
Evaluate (3 + 4) * 2, then ask Lean for the type of the same expression. Read both answers in Output.
Suggested steps
- Evaluate the expression with #eval
- Inspect 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