grewriteLocalDecl — Mathlib

Lean4
/-- Apply the `grewrite` tactic to a local hypothesis. -/
def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : GRewrite.Config) : TacticM Unit :=
  withMainContext do
    -- Note: we cannot execute `replace` inside `Term.withSynthesize`.
      -- See issues https://github.com/leanprover-community/mathlib4/issues/2711 and https://github.com/leanprover-community/mathlib4/issues/2727.

    let goal ← getMainGoal
    let r ←
      Term.withSynthesize <|
          withMainContext do
            let e ← elabTerm stx none true
            if e.hasSyntheticSorry then
              throwAbortTactic
            let localDecl ← fvarId.getDecl
            goal.grewrite localDecl.type e (forwardImp := true) (symm := symm) (config := config)
    let proof := .app (r.impProof) (.fvar fvarId)
    let { mvarId, .. } ← goal.replace fvarId proof r.eNew
    replaceMainGoal (mvarId :: r.mvarIds)
Похожие утверждения