Documentation

Lean.Meta.Tactic.Simp.LoopProtection

@[inline]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.Simp.checkLoops (force : Bool) (ctxt : Context) (methods : Methods) (thm : SimpTheorem) :

Main entry point to the loop protection mechanism: Checks if the given theorem is looping in the current simp set, and logs a warning if it does.

Assumes that withRef is set appropriately for the warning.

With force := off, only runs when linter.loopingSimpArgs is enabled and presents it as a linter. With force := on (typically after simp threw an exception) it prints plain warnings.

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