insertProof — Mathlib

Lean4
/-- Generalize `prop`, where `proof` is its proof.
-/
def insertProof (prop pf : Expr) : MAbs Unit := do
  if (← read).config.debug then
    unless ← isDefEq prop (← inferType pf) do
      throwError "insertProof: proof{(indentD pf)}does not have type{indentD prop}"
    unless ← Lean.MetavarContext.isWellFormed (← read).initLCtx pf do
      throwError "insertProof: proof{(indentD pf)}\nis not well-formed in the initial context\n\
                  fvars: {(← read).fvars}"
    unless ← Lean.MetavarContext.isWellFormed (← read).initLCtx prop do
      throwError "insertProof: proof{(indentD prop)}\nis not well-formed in the initial context\n\
                  fvars: {(← read).fvars}"
  modify fun s ↦
      { s with
        generalizations := s.generalizations.push (prop, pf)
        propToProof := s.propToProof.insert prop pf }
Похожие утверждения