getExprInputs

Mathlib.Tactic.MoveAdd

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

Lean4

/-- `getExprInputs e` inspects the outermost constructor of `e` and returns the array of all the
arguments to that constructor that are themselves `Expr`essions. -/
def getExprInputs : Expr → Array Expr
  | app fn arg => #[fn, arg]
  | lam _ bt bb _ => #[bt, bb]
  | forallE _ bt bb _ => #[bt, bb]
  | letE _ t v b _ => #[t, v, b]
  | mdata _ e => #[e]
  | proj _ _ e => #[e]
  | _ => #[]

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

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

Разделы

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

Аффилиация

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