Commit 2023-09-10 13:09 2677935b

View on Github →

refactor: re-home some meta code (#6921)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.letDepth

added def Lean.Expr.sides?

Modified Mathlib/Lean/Meta.lean

added def Lean.MVarId.iffOfEq

added def Lean.MVarId.proofIrrelHeq

added def Lean.MVarId.propext

added def Lean.MVarId.subsingletonElim

Created Mathlib/Lean/Meta/CongrTheorems.lean

added def Lean.Meta.mkHCongrWithArity'

Modified Mathlib/Tactic/Congr!.lean

deleted def Lean.MVarId.iffOfEq

deleted def Lean.MVarId.liftReflToEq

deleted def Lean.MVarId.proofIrrelHeq

deleted def Lean.MVarId.propext

deleted theorem Lean.MVarId.rel_of_eq_and_refl

deleted def Lean.MVarId.subsingletonElim

Modified Mathlib/Tactic/ExtractLets.lean

deleted def Lean.Expr.letDepth

Modified Mathlib/Tactic/Relation/Rfl.lean

added def Lean.MVarId.liftReflToEq

Modified Mathlib/Tactic/TermCongr.lean

deleted def Mathlib.Tactic.TermCongr.mkHCongrWithArity'

deleted def Mathlib.Tactic.TermCongr.sides?