mkApps

Mathlib.Tactic.CC.Datatypes

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

Lean4

/-- Sorts `args` and applies them to `ACApps.apps`. -/
def mkApps (op : Expr) (args : Array Expr) : ACApps :=
  .apps op (args.qsort Expr.lt)

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

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

Разделы

Аффилиация

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