isCoeFun

Mathlib.Tactic.FunProp.Mor

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

Lean4

/-- Is `e` a coercion from some function space to functions? -/
def isCoeFun (e : Expr) : MetaM Bool := do
  let some (name, _) := e.getAppFn.const? |
    return false
  let some info ← getCoeFnInfo? name |
    return false
  return e.getAppNumArgs' + 1 == info.numArgs

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

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

Разделы

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

Аффилиация

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