runAndFailIfNoProgress — Mathlib

Lean4
/-- Run `tacs : TacticM Unit` on `goal`, and fail if no progress is made. -/
def runAndFailIfNoProgress (goal : MVarId) (tacs : TacticM Unit) : TacticM (List MVarId) := do
  let l ← run goal tacs
  try
    let [newGoal] := l |
      failure
    goal.withContext do
        -- Check that the local contexts are compatible

        let ctxDecls := (← goal.getDecl).lctx.decls.toList
        let newCtxDecls := (← newGoal.getDecl).lctx.decls.toList
        guard <| ← withNewMCtxDepth <| withReducible <| lctxIsDefEq ctxDecls newCtxDecls
        guard <| ← withNewMCtxDepth <| withReducible <| isDefEq (← newGoal.getType) (← goal.getType)
  catch _ =>
    return l
  throwError "no progress made on\n{goal}"
Похожие утверждения