dabstract — Mathlib

Lean4
/-- Analogue of `kabstract` with support for inserting casts. -/
def dabstract (e : Expr) (p : Expr) (cfg : DepRewrite.Config) : MetaM Expr := do
  let e ← instantiateMVars e
  let tp ← inferType p
  withTraceNode traceCls
      (fun
        -- Message shows unified pattern (without mvars) b/c it is constructed after the body runs

        | .ok motive => pure m! "{e } =[x/{p }]=> {motive}"
        | .error (err : Lean.Exception) => pure m! "{e } =[x/{p }]=> 💥️{indentD err.toMessageData}")
      do
      withLocalDeclD `x tp fun x => do
          withLocalDeclD `h (← mkEq p x) fun h => do
              let e' ← visit e none |>.run { cfg, p, x, h, Δ := ∅, δ := ∅ } |>.run.run' 1
              mkLambdaFVars #[x, h] e'
Похожие утверждения