getCongrAppFnArgs

Mathlib.Tactic.GCongr.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GCongr.getCongrAppFnArgs

Lean4

/-- Given an application `f a₁ .. aₙ`, return the name of `f`, and the array of arguments `aᵢ`. -/
def getCongrAppFnArgs (e : Expr) : Option (Name × Array Expr) :=
  match e.cleanupAnnotations with
  | .forallE n d b bi =>
    -- We determine here whether an arrow is an implication or a forall
        -- this approach only works if LHS and RHS are both dependent or both non-dependent
    if b.hasLooseBVars then some (`_Forall, #[.lam n d b bi]) else some (`_Implies, #[d, b])
  | e => e.withApp fun f args => f.constName?.map (·, args)

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

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

Разделы

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

Аффилиация

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