# 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.

```lean
#check 5
#check "Lean"
#check true
#check Nat
```

Typical output:

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

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

## Checking Functions

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

Output:

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

This tells you how to apply the function.

## Checking Applications

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

Output:

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

`#check` confirms both the validity and the result type.

## Checking Definitions

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

#check double
#check double 5
```

Output:

```text
double : Nat -> Nat
double 5 : Nat
```

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

## Checking Theorems

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

#check id_prop
#check id_prop True
```

Output:

```text
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.

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

#check idImplicit
```

Output:

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

To see all arguments explicitly:

```lean
#check @idImplicit
```

Output:

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

The `@` form exposes implicit parameters.

## Checking Overloaded Notation

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

```lean
#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.

```lean
#check Nat
#check Nat -> Nat
#check List Nat
#check Prop
```

Output:

```text
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.

```lean
#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.

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

This reveals:

```text
hp : P
hpq : P -> Q
```

Use this to understand the current context.

## Checking Structures and Fields

```lean
structure Point where
  x : Nat
  y : Nat

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

Output:

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

This shows how to access structure fields.

## Checking Typeclass-Driven Expressions

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

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

## `#check` vs `#eval`

| Command  | Purpose       |
| -------- | ------------- |
| `#check` | show type     |
| `#eval`  | compute value |

Example:

```lean
#check 2 + 3
#eval 2 + 3
```

Output:

```text
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

```lean
#check subexpr
```

2. Add type annotations

```lean
#check (subexpr : ExpectedType)
```

3. Inspect function types

```lean
#check function
```

4. Expand implicit arguments

```lean
#check @function
```

This isolates where the mismatch occurs.

## Recipe: Explore a Library Function

When using a new function:

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

Then apply it:

```lean
#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.