getFnConstName?

Mathlib.Tactic.FunProp.FunctionData

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.FunctionData.getFnConstName?

Lean4

/-- Is head function of `f` a constant?

If the head of `f` is a projection return the name of corresponding projection function. -/
def getFnConstName? (f : FunctionData) : MetaM (Option Name) := do
  match f.fn with
  | .const n _ =>
    return n
  | .proj typeName idx _ =>
    let some info := getStructureInfo? (← getEnv) typeName |
      return none
    let some projName := info.getProjFn? idx |
      return none
    return projName
  | _ =>
    return none

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

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

Разделы

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

Аффилиация

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