Explicit Parameter (Lean)

Definition

Explicit parameter (Lean)

In a Lean declaration, (x : T) introduces an explicit parameter named x of type T. A caller normally supplies its argument directly: if f has this parameter, f t supplies x := t.

Unlike an implicit parameter or instance-implicit parameter, it is not normally omitted from an application. Writing _ explicitly asks elaboration to infer the argument instead; inference must have enough information to determine it.