Commit 2026-02-02 23:29 6a1be367

View on Github →

chore: deprecate memoFix and replaceRec (#34384) This deprecation was requested by Floris van Doorn in #33236

Estimated changes

Modified Mathlib/Lean/Expr.lean

Modified Mathlib/Lean/Expr/ReplaceRec.lean

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean

Modified Mathlib/Util/MemoFix.lean

Deleted MathlibTest/Expr.lean

deleted def bar

deleted def foo

deleted def reorderLastArguments