Def Lean.Expr.rewriteType

Modification history

2025-10-04 07:54
Mathlib/Lean/Expr/Basic.lean
chore(Lean/Expr/Basic): move material about rewriting to a new file (#30156) …
Modified Lean.Expr.rewriteTypeView on Github →
2023-05-06 12:10
Mathlib/Lean/Expr/Basic.lean
feat: enable cancel_denoms preprocessor in linarith (#3801) …
Added Lean.Expr.rewriteTypeView on Github →