ACApps

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.ACApps

Lean4

/-- An `ACApps` represents either just an `Expr` or applications of an associative and commutative
  binary operator. -/
inductive ACApps where/-- An `ACApps` of just an `Expr`. -/

  | ofExpr (e : Expr) : ACApps/-- An `ACApps` of applications of a binary operator. `args` are assumed to be sorted.

    See also `ACApps.mkApps` if `args` are not yet sorted. -/

  | apps (op : Expr) (args : Array Expr) : ACApps
  deriving Inhabited, BEq

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

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

Разделы

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

Аффилиация

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