1.13 Checking Types with `#check`

Type checking is the primary feedback mechanism in Lean. Before evaluating or proving anything, you should know the exact type of each expression. The command #check asks Lean to infer and display that type.

Problem

You want to understand what an expression means in Lean, diagnose type errors, and inspect functions, theorems, and intermediate terms.

Solution

Use #check on any expression.

#check 5
#check "Lean"
#check true
#check Nat

Typical output:

5 : Nat
"Lean" : String
true : Bool
Nat : Type

#check does not evaluate the expression. It only reports its type.

Checking Functions

#check Nat.succ
#check (fun x : Nat => x + 1)

Output:

Nat.succ : Nat -> Nat
fun x => x + 1 : Nat -> Nat

This tells you how to apply the function.

Checking Applications

#check Nat.succ 3
#check (fun x : Nat => x + 1) 10

Output:

Nat.succ 3 : Nat
(fun x => x + 1) 10 : Nat

#check confirms both the validity and the result type.

Checking Definitions

def double (n : Nat) : Nat :=
  n + n

#check double
#check double 5

Output:

double : Nat -> Nat
double 5 : Nat

Use this to confirm that a definition has the intended type.

Checking Theorems

theorem id_prop (P : Prop) : P -> P := by
  intro h
  exact h

#check id_prop
#check id_prop True

Output:

id_prop : (P : Prop) -> P -> P
id_prop True : True -> True

A theorem behaves like a function whose inputs are proofs and whose output is a proof.

Inspecting Implicit Arguments

Many arguments are implicit. Use #check to see how Lean presents them.

def idImplicit {α : Type} (x : α) : α :=
  x

#check idImplicit

Output:

idImplicit : {α : Type} -> α -> α

To see all arguments explicitly:

#check @idImplicit

Output:

@idImplicit : (α : Type) -> α -> α

The @ form exposes implicit parameters.

Checking Overloaded Notation

Operators are often overloaded. Use #check to resolve them.

#check (2 + 3)
#check (2 : Nat) + (3 : Nat)
#check (2 : Int) + (3 : Int)

Each expression may refer to a different underlying function depending on the type.

Checking Types Themselves

Types are also expressions.

#check Nat
#check Nat -> Nat
#check List Nat
#check Prop

Output:

Nat : Type
Nat -> Nat : Type
List Nat : Type
Prop : Type

This confirms that Lean treats types uniformly.

Checking Partial Expressions

You can use _ as a placeholder.

#check (fun x : Nat => _)

Lean reports the expected type for the hole. This is useful when constructing expressions incrementally.

Checking in Context

Inside a proof or definition, #check can inspect local variables.

theorem example (P Q : Prop) (hp : P) (hpq : P -> Q) : Q := by
  #check hp
  #check hpq
  exact hpq hp

This reveals:

hp : P
hpq : P -> Q

Use this to understand the current context.

Checking Structures and Fields

structure Point where
  x : Nat
  y : Nat

#check Point
#check Point.x
#check Point.y

Output:

Point : Type
Point.x : Point -> Nat
Point.y : Point -> Nat

This shows how to access structure fields.

Checking Typeclass-Driven Expressions

#check (0 : Nat)
#check (0 : Int)

Numeric literals depend on typeclass instances. #check confirms which instance is used.

#check vs #eval

Example:

#check 2 + 3
#eval 2 + 3

Output:

2 + 3 : Nat
5

Use #check first to ensure the expression is well-typed, then #eval to compute it.

Recipe: Diagnose a Type Error

If Lean reports a type mismatch:

1. Check subexpressions

#check subexpr

2. Add type annotations

#check (subexpr : ExpectedType)

3. Inspect function types

#check function

4. Expand implicit arguments

#check @function

This isolates where the mismatch occurs.

Recipe: Explore a Library Function

When using a new function:

#check List.map
#check List.map (fun x : Nat => x + 1)

Then apply it:

#eval List.map (fun x : Nat => x + 1) [1, 2, 3]

This pattern avoids guessing argument order and types.

Common Pitfalls

If #check fails, the expression is ill-typed.

If the type is more general than expected, implicit arguments may be involved.

If the type is ambiguous, add a type ascription.

If the result is hard to read, use #check @name to expose all parameters.

If names are not found, verify imports and namespaces.

Takeaway

#check is the primary tool for understanding Lean code. It reveals types, clarifies implicit arguments, and exposes how expressions are interpreted. Regular use of #check reduces trial and error and makes development systematic.