4.8. Tactic.EqLift.Tactic.Location
Tactic location support
This module provides utilities for applying tactics to multiple goals and hypotheses
specified by location patterns, following the standard Lean syntax (like in rw or simp).
Main declarations
-
applyLocTactic: applies a tactic to goals and hypotheses at specified locations.
Module LeanMachineLearning.Tactic.EqLift.Tactic.Location contains 2 exposed declarations.