tryTheoremCore — Mathlib

Lean4
/-- Try to apply theorem - core function -/
def tryTheoremCore (xs : Array Expr) (val : Expr) (type : Expr) (e : Expr) (thmId : Origin)
    (funProp : Expr → FunPropM (Option Result)) : FunPropM (Option Result) := do
  withTraceNode `Meta.Tactic.fun_prop (fun r => return s! "[{ExceptToEmoji.toEmoji r}] applying: {← ppOrigin' thmId}")
      (do
        if (← isDefEq type e) then
          if ¬(← synthesizeArgs thmId xs funProp) then
            return none
          let proof ← instantiateMVars (mkAppN val xs)
          return some { proof := proof }
        else
          trace[Meta.Tactic.fun_prop]"failed to unify {(← ppOrigin thmId)}\n{type }\nwith\n{e}"
          return none)
Похожие утверждения