cleanup — Mathlib

Lean4
/-- A cleanup routine, which simplifies expressions in `abel` normal form to a more human-friendly
format. -/
def cleanup (cfg : AbelNF.Config) (r : Simp.Result) : MetaM Simp.Result := do
  match cfg.mode with
  | .raw =>
    pure r
  | .term =>
    let thms := [``term_eq, ``termg_eq, ``add_zero, ``one_nsmul, ``one_zsmul, ``zsmul_zero]
    let ctx ←
      Simp.mkContext (config := { zetaDelta := cfg.zetaDelta }) (simpTheorems := #[← thms.foldlM (·.addConst ·) { }])
          (congrTheorems := ← getSimpCongrTheorems)
    pure <| ← r.mkEqTrans (← Simp.main r.expr ctx (methods := ← Lean.Meta.Simp.mkDefaultMethods)).1
Похожие утверждения