Documentation

Lean.Elab.Tactic.Location

Denotes a set of locations where a tactic should be applied for the main goal. See also withLocation.

Instances For

    Runs the given atLocal and atTarget methods on each of the locations selected by the given loc. If any of the selected tactic applications fail, it will call failed with the main goal mvar.

    Instances For