Commit 2023-09-19 12:32 904dc41a

View on Github →

port the clean tactic from lean 3 to lean 4 (#5909)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Clean.lean

added def Lean.Expr.clean

added def Lean.Expr.cleanConsts

added def Mathlib.Tactic.elabClean

Created test/Clean.lean

added def Tests.withClean

added def Tests.withoutClean

added def Tests.x'

added def Tests.x