isCoeFunName

Mathlib.Tactic.FunProp.Mor

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

Lean4

/-- Is `name` a coercion from some function space to functions? -/
def isCoeFunName (name : Name) : CoreM Bool := do
  let some info ← getCoeFnInfo? name |
    return false
  return info.type == .coeFun

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

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

Разделы

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

Аффилиация

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