Documentation

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 #

source
def replaceEquality (goal : Lean.MVarId) (fvarId : Option Lean.FVarId) (transform : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)) :
Lean.Elab.Tactic.TacticM Lean.MVarId

Replace an equality in a goal or hypothesis with a transformed expression, using a provided transformation function.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def applyLocTactic (loc : Lean.Elab.Tactic.Location) (transform : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)) :
    Lean.Elab.Tactic.TacticM Unit

    Apply a given transformation to all goals and/or hypotheses specified by a Location.

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