Implicit Parameter (Lean)

Definition

Implicit parameter (Lean)

In a Lean declaration, {x : T} introduces an implicit parameter named x of type T. When its argument is omitted, elaboration inserts a placeholder and tries to determine its value by matching types using the other arguments and the expected result type.

Unlike an explicit parameter, its argument is normally omitted, but still exists in the resulting expression. It can be supplied explicitly as f (x := t); if the available information does not determine it, the caller must provide more information. Unlike an instance-implicit parameter, this syntax does not request instance synthesis.