Skip to content

1.9 Implicit and Explicit Arguments

Lean functions often contain arguments that the user does not write.

lean proof-assistant type-theory functional-programming

Lean functions often contain arguments that the user does not write. These are implicit arguments. They are reconstructed by elaboration from the surrounding context. Explicit arguments are written directly by the user. Good Lean code uses both: explicit arguments for data that matters to the reader, implicit arguments for information that Lean can infer reliably.

Problem

You want to understand why some arguments are written, why some are omitted, and how to recover control when Lean cannot infer the omitted information.

Solution

Use parentheses for explicit arguments and braces for implicit arguments.

def idExplicit (α : Type) (x : α) : α :=
  x

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

The first definition requires the type argument:

#check idExplicit Nat 3

The second lets Lean infer it:

#check idImplicit 3

Lean infers α = Nat from the argument 3.

Explicit Arguments

An explicit argument is enclosed in ordinary parentheses, or written without brackets in a function type.

def addExplicit (x : Nat) (y : Nat) : Nat :=
  x + y

Both arguments must be supplied.

#eval addExplicit 2 5

Expected result:

7

The type of addExplicit is:

#check addExplicit

which reports:

addExplicit : Nat -> Nat -> Nat

The arguments are explicit because the function cannot do useful work unless the caller supplies both numbers.

Implicit Arguments

An implicit argument is enclosed in braces.

def first {α β : Type} (x : α) (y : β) : α :=
  x

The caller writes only the data arguments:

#check first 10 true

Lean infers:

α = Nat
β = Bool

So the expression has type:

first 10 true : Nat

The type arguments are omitted because they are recoverable from 10 and true.

Seeing All Arguments with @

The @ symbol disables implicit insertion and exposes all arguments.

#check @first

Lean reports a type similar to:

@first : {α β : Type} -> α -> β -> α

You can then supply implicit arguments explicitly:

#check @first Nat Bool 10 true

This is useful when elaboration fails or when you want to inspect the complete type of a declaration.

When Inference Works

Implicit inference works best when an omitted argument appears in the type of a later explicit argument.

def last {α : Type} (x y : α) : α :=
  y

In the call:

#check last 1 2

Lean infers α = Nat from the arguments 1 and 2.

Similarly:

#check last "a" "b"

Lean infers α = String.

When Inference Fails

Inference may fail when the implicit argument does not appear in enough explicit information.

def makeEmpty {α : Type} : List α :=
  []

The expression:

#check makeEmpty

has an ambiguous element type. Lean may keep the type as a metavariable, or it may require more context.

Give the type explicitly:

#check (makeEmpty : List Nat)

or expose the implicit argument:

#check @makeEmpty Nat

Both tell Lean that α = Nat.

Type Ascription as Guidance

A type ascription is often the cleanest way to guide inference.

def emptyNatList : List Nat :=
  makeEmpty

The expected type List Nat determines the implicit argument.

This pattern is preferred when the result type is part of the surrounding code. It keeps the call readable and lets the type annotation do the work.

Explicit Type Arguments in Calls

Sometimes you want to provide only one implicit argument while leaving others inferred. Lean supports named arguments.

def pairWithDefault {α : Type} [Inhabited α] (x : α) : α × α :=
  (default, x)

You can write:

#check pairWithDefault (α := Nat) 5

This tells Lean which type to use for α.

Named arguments are useful when a function has several implicit parameters and @ would make the call noisy.

Instance Implicit Arguments

Square brackets mark typeclass arguments.

def defaultValue {α : Type} [Inhabited α] : α :=
  default

The argument [Inhabited α] is found by typeclass search.

#eval (defaultValue : Nat)
#eval (defaultValue : Bool)

Lean uses available instances for Nat and Bool.

This is a different mechanism from ordinary implicit inference. The type α is inferred from context, and the instance [Inhabited α] is then found by search.

Strict Implicit Arguments

Double braces mark strict implicit arguments.

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

A strict implicit argument is inserted only when a later explicit argument is present. This prevents Lean from inserting metavariables too early.

Strict implicit arguments are less common in beginner code, but they appear in libraries where elaboration order matters.

Output Parameters and Typeclasses

Some typeclass arguments depend on earlier arguments.

#check OfNat.ofNat

Numeric literals use typeclass machinery. The literal 0 can mean a natural number, integer, rational number, or another type with a suitable instance.

Context determines the type:

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

When context is missing, Lean may report ambiguity. Add a type ascription.

Recipe: Make Types Implicit, Data Explicit

A common design rule is:

def mapPair {α β : Type} (f : α -> β) (p : α × α) : β × β :=
  (f p.1, f p.2)

The types α and β are implicit because Lean can infer them from f and p. The function and pair are explicit because they are the actual data.

Use:

#eval mapPair (fun n : Nat => n + 1) (3, 4)

Expected result:

(4, 5)

Recipe: Use Explicit Arguments for Ambiguous Control

Some arguments affect behavior but may not be inferable.

def repeatValue (α : Type) (n : Nat) [Inhabited α] : List α :=
  List.replicate n default

Here α is explicit because the output type may not provide enough context at the call site.

#eval repeatValue Nat 3
#eval repeatValue Bool 3

Expected results:

[0, 0, 0]
[false, false, false]

Making α explicit improves usability in this case.

Inspecting a Declaration

When unsure, inspect the declaration.

#check first
#check @first

The first form shows the usual call shape. The second form shows all parameters.

For library declarations, this is often the fastest way to understand why a call fails.

Common Pitfalls

If Lean says it cannot synthesize an instance, an argument in square brackets could not be found by typeclass search.

If Lean says it cannot infer a metavariable, an implicit argument lacks enough context.

If a function call has too many arguments, some arguments may already be implicit.

If a function call has too few arguments, inspect the full type with #check @name.

If a numeric literal is ambiguous, add a type ascription such as (0 : Nat).

Takeaway

Explicit arguments are written by the caller. Implicit arguments are reconstructed by elaboration. Ordinary implicit arguments use braces, typeclass arguments use square brackets, and @ exposes the full argument list. Good Lean interfaces make predictable information implicit and meaningful data explicit.