Def Lean.Expr.size

Modification history

2025-09-06 22:14

Mathlib/Tactic/MoveAdd.lean

chore(Tactic.MoveAdd): deprecate Expr.size (#29358) …

Deleted Lean.Expr.size View on Github →

2023-10-09 12:27

Mathlib/Tactic/MoveAdd.lean

feat(Tactic/MoveAdd): port `move_add` (#6576) …

Added Lean.Expr.size View on Github →