size

Mathlib.Tactic.MoveAdd

URI: https://scilib.ai/kg/mathlib#Lean.Expr.size

Lean4

/-- `size e` returns the number of subexpressions of `e`. -/
@[deprecated Lean.Expr.sizeWithoutSharing (since := "2025-09-04")]
partial def size (e : Expr) : ℕ :=
  (e.getExprInputs.map size).foldl (· + ·) 1

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru