Instance-Implicit Parameter (Lean)

Definition

Instance-implicit parameter (Lean)

In a Lean declaration, [x : T] introduces an instance-implicit parameter of class type T. When its argument is omitted, Lean uses instance synthesis to find a term of type T and insert it. Within the parameter’s scope, x is itself available as a local instance. [T] leaves the parameter unnamed.

Unlike an implicit parameter, it requests instance search rather than only inference from type constraints. Unlike an explicit parameter, its argument is normally omitted. Use this binder when the supplied value should be available to operations requiring an instance of T; a named argument can still be supplied explicitly as f (x := t).

This is an ordinary argument passed automatically, not a different kind of mathematical assumption.