bvarAppCase

Mathlib.Tactic.FunProp.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.bvarAppCase

Lean4

/-- Prove function property of `fun f => f x₁ ... xₙ`. -/
def bvarAppCase (funPropDecl : FunPropDecl) (e : Expr) (fData : FunctionData)
    (funProp : Expr → FunPropM (Option Result)) : FunPropM (Option Result) := do
  if (← fData.isMorApplication) != .none then
    applyMorRules funPropDecl e fData funProp
  else
    if let some (f, g)← fData.nontrivialDecomposition then
      applyCompRule funPropDecl e f g funProp
    else
      applyApplyRule funPropDecl e funProp

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

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

Разделы

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

Аффилиация

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