isFunPropGoal

Mathlib.Tactic.FunProp.Decl

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

Lean4

/-- Is `e` a `fun_prop` goal? For example `∀ y z, Continuous fun x => f x y z` -/
def isFunPropGoal (e : Expr) : MetaM Bool := do
  forallTelescope e fun _ b => return (← getFunProp? b).isSome

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

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

Разделы

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

Аффилиация

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