# Fail if no progress #

This implements the `fail_if_no_progress` tactic, which fails if no actual progress is made by the following tactic sequence.

"Actual progress" means that either the number of goals has changed, that the number or presence of expressions in the context has changed, or that the type of some expression in the context or the type of the goal is no longer definitionally equal to what it used to be at reducible transparency.

This means that, for example, `1 - 1` changing to `0` does not count as actual progress, since

    example : (1 - 1 = 0) := by with_reducible rfl

This tactic is useful in situations where we want to stop iterating some tactics if they're not having any effect, e.g. `repeat (fail_if_no_progress simp <;> ring_nf)`.

source
def Mathlib.Tactic.failIfNoProgress :
Lean.ParserDescr

`fail_if_no_progress tacs` evaluates `tacs`, and fails if no progress is made on the main goal or the local context at reducible transparency.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[irreducible]
def Mathlib.Tactic.lctxIsDefEq (l₁ l₂ : List (Option Lean.LocalDecl)) :
Lean.MetaM Bool

`lctxIsDefEq l₁ l₂` compares two lists of `Option LocalDecl`s (as returned from e.g. `(← (← getMainGoal).getDecl).lctx.decls.toList`). It returns `true` if they have the same local declarations in the same order (up to defeq, without setting mvars), and `false` otherwise.

Assumption: this function is run with one of the local contexts as the current `MetaM` local context, and one of the two lists consists of the `LocalDecl`s of that context.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.lctxIsDefEq (none :: l₁) x✝ = Mathlib.Tactic.lctxIsDefEq l₁ x✝
- Mathlib.Tactic.lctxIsDefEq x✝ (none :: l₂) = Mathlib.Tactic.lctxIsDefEq x✝ l₂
- Mathlib.Tactic.lctxIsDefEq [] [] = pure true
- Mathlib.Tactic.lctxIsDefEq x✝¹ x✝ = pure false

Instances For

source
def Mathlib.Tactic.runAndFailIfNoProgress (goal : Lean.MVarId) (tacs : Lean.Elab.Tactic.TacticM Unit) :
Lean.Elab.Tactic.TacticM (List Lean.MVarId)

Run `tacs : TacticM Unit` on `goal`, and fail if no progress is made.

Equations

- One or more equations did not get rendered due to their size.

Instances For