opaque Lean.Meta.Simp.linter.loopingSimpArgs : Lean.Option Bool

@[inline]

def Lean.Meta.Simp.withFreshUsedTheorems {α : Type} (x : SimpM α) : SimpM α

Equations

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

def Lean.Meta.Simp.mkLoopWarningMsg (thm : SimpTheorem) : SimpM MessageData

Equations

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

def Lean.Meta.Simp.shouldCheckLoops (force : Bool) (ctxt : Context) : CoreM Bool

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) : MetaM Unit

Main entry point to the loop protection mechanis: 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.