Documentation

Batteries.Tactic.Instances

#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.

#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.
Instances For

    #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.
    Instances For