withIncreasedTransitionDepth — Mathlib

Lean4

/-- Increase transition depth. Return `none` if maximum transition depth has been reached. -/
def withIncreasedTransitionDepth {α} (go : FunPropM (Option α)) : FunPropM (Option α) := do
  let maxDepth := (← read).config.maxTransitionDepth
  let newDepth := (← read).transitionDepth + 1
  if newDepth > maxDepth then
    trace[Meta.Tactic.fun_prop]"maximum transition depth ({maxDepth }) reached
          if you want `fun_prop` to continue then increase the maximum depth with \
          `fun_prop (maxTransitionDepth := {newDepth})`"
    return none
  else
    withReader (fun s => { s with transitionDepth := newDepth }) go

Похожие утверждения