Ask Lean about types

Every expression in Lean has a type, and #check is how you ask for it. It elaborates the expression and prints expression : type. Nothing is run. #eval is the other half of the pair: it runs the expression and prints the value, which only works when the result is something Lean knows how to display.

A function comes back described the way it was declared. #check double answers double (n : Nat) : Nat, naming the parameter. Apply it and the answer changes: #check double 3 answers double 3 : Nat, because the argument is supplied and what is left is a number.

Types are expressions too, so you can ask about them. #check Nat answers Nat : Type. #check (2 + 2 = 4) answers 2 + 2 = 4 : Prop. That distinction carries the rest of the Academy: Type classifies data, Prop classifies statements, and a value whose type is a Prop is a proof of it.

This is also the fastest way to understand an error. When two things do not fit, ask for the type of each piece on its own. The mismatch is usually obvious once both answers are in front of you.

Worked example

#check 42              -- 42 : Nat
#check "Lean"          -- "Lean" : String
#check true            -- Bool.true : Bool

#check greet           -- greet (name : String) : String
#eval greet "Lean"     -- "Hello, Lean"

#check Nat             -- Nat : Type
#check Prop            -- Prop : Type
#check (2 + 2 = 4)     -- 2 + 2 = 4 : Prop

Look at #check true: Lean answers Bool.true, the constructor’s full name, not the text you typed. #check reports what the expression elaborates to. Your exercise asks the three kinds of question about double: the function itself, the function applied to something, and a claim about the result.