Foundations · 5 min
Values and types
Lean is both a programming language and a proof assistant. You can calculate with it, write applications, and express claims that the type checker verifies.
Every expression has a type. Nat is the type of natural numbers. A colon introduces a type annotation, and := provides the value of a definition. #eval executes an expression; #check tells you its type.
Exercise
Define answer as a natural number equal to 42. Use a literal or an arithmetic expression.
Open exercise in editordef answer : Nat := 0
#eval answer
Hint
Replace 0 with 6 * 7. Nat multiplication uses *.
Solution
def answer : Nat := 6 * 7
#eval answer