#instances command

The #instances command prints lists all instances that apply to the given type, if it is a class. It is similar to #synth but it only does the very first step of the instance synthesis algorithm, which is to enumerate potential instances.

def Std.Tactic.Instances.instancesCmd : Lean.ParserDescr

#instances term prints all the instances for the given class. For example, #instances Add _ gives all Add instances, and #instances Add Nat gives the Nat instance. The term can be any type that can appear in [...] binders.

Trailing underscores can be omitted, and #instances Add and #instances Add _ are equivalent; the command adds metavariables until the argument is no longer a function.

The #instances command is closely related to #synth, but #synth does the full instance synthesis algorithm and #instances does the first step of finding potential instances.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.Instances.«command#instances__:_» : Lean.ParserDescr

#instances term prints all the instances for the given class. For example, #instances Add _ gives all Add instances, and #instances Add Nat gives the Nat instance. The term can be any type that can appear in [...] binders.

Trailing underscores can be omitted, and #instances Add and #instances Add _ are equivalent; the command adds metavariables until the argument is no longer a function.

The #instances command is closely related to #synth, but #synth does the full instance synthesis algorithm and #instances does the first step of finding potential instances.

Equations

• One or more equations did not get rendered due to their size.