app7?

Mathlib.Tactic.Widget.CommDiag

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

Lean4

/-- If the expression is a function application of `fName` with 7 arguments, return those arguments.
Otherwise return `none`. -/
@[inline]
def _root_.Lean.Expr.app7? (e : Expr) (fName : Name) : Option (Expr × Expr × Expr × Expr × Expr × Expr × Expr) :=
  if e.isAppOfArity fName 7 then
    some
      (e.appFn!.appFn!.appFn!.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appFn!.appFn!.appFn!.appArg!,
        e.appFn!.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appArg!,
        e.appFn!.appArg!, e.appArg!)
  else none

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

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

Разделы

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

Аффилиация

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