- wildcard: Lean.Elab.Tactic.Location
Apply the tactic everywhere.
- targets: Array Lean.Syntax → Bool → Lean.Elab.Tactic.Location
hypothesesare hypothesis names in the main goal that the tactic should be applied to. If
typeis true, then the tactic should also be applied to the target type.
Denotes a set of locations where a tactic should be applied for the main goal. See also
Runs the given
atTarget methods on each of the locations selected by the given
If any of the selected tactic applications fail, it will call
failed with the main goal mvar.