applyTransitionRules — Mathlib

Lean4

/-- Prove function property of using *transition theorems*. -/
def applyTransitionRules (e : Expr) (funProp : Expr → FunPropM (Option Result)) : FunPropM (Option Result) := do
  withIncreasedTransitionDepth
      (do
        let candidates ← getTransitionTheorems e
        trace[Meta.Tactic.fun_prop]"candidate transition theorems: {←
            candidates.mapM fun c => ppOrigin (.decl c.thmName)}"
        for c in candidates do
          if let some r← tryTheorem? e (.decl c.thmName) funProp then
            return r
        trace[Debug.Meta.Tactic.fun_prop]"no theorem matched"
        return none)

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