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
    Equations
    • One or more equations did not get rendered due to their size.
    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.

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