Getting started
Values & types
Evaluate expressions with #eval and inspect their types with #check.
Open Values.lean in editor-- #eval runs an expression
#eval 6 * 7
#eval "Lean" ++ " is a language"
#eval [1, 2, 3].length
-- #check reports a type
#check 42
#check "hello"
#check true
Explanation
#eval
Evaluates an expression and shows the result in the message output.
#check
Elaborates an expression and shows its type without running it.
++
Appends strings or lists. Lean chooses the operation from the types.
Expected output
Reference only. Run the file to check its actual result.
42 "Lean is a language" 3 42 : Nat "hello" : String Bool.true : Bool
Exercise
Evaluate 2 ^ 10. Then check the type of [1, 2, 3].