Commit 2025-09-06 22:14 3f99589d
View on Github →chore(Tactic.MoveAdd): deprecate Expr.size (#29358)
Deprecate Lean.Expr.size. It is equivalent to Lean.Expr.sizeWithoutSharing, but slower because it constructs an intermediate array.
chore(Tactic.MoveAdd): deprecate Expr.size (#29358)
Deprecate Lean.Expr.size. It is equivalent to Lean.Expr.sizeWithoutSharing, but slower because it constructs an intermediate array.