applyConstRule — Mathlib

Lean4
/-- Try to prove `e` using the *constant lambda theorem*.

For example, `e = q(Continuous fun x => y)` and `funPropDecl` is `FunPropDecl` for `Continuous`.
-/
def applyConstRule (funPropDecl : FunPropDecl) (e : Expr) (funProp : Expr → FunPropM (Option Result)) :
    FunPropM (Option Result) := do
  let thms ← getLambdaTheorems funPropDecl.funPropName .const
  if thms.size = 0 then
    let msg := s!"missing constant rule to prove `{← ppExpr e}`"
    logError msg
    trace[Meta.Tactic.fun_prop]
    return none
  for thm in thms do
    let .const := thm.thmArgs |
      return none
    if let some r← tryTheorem? e (.decl thm.thmName) funProp then
      return r
  return none
Похожие утверждения