mkKind

Mathlib.Tactic.Widget.StringDiagram

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Widget.StringDiagram.mkKind

Lean4

/-- Given an expression, return the kind of the context. -/
def mkKind (e : Expr) : MetaM Kind := do
  let e ← instantiateMVars e
  let e ←
    (match (← whnfR e).eq? with
      | some (_, lhs, _) => return lhs
      | none => return e)
  let ctx? ← BicategoryLike.mkContext? (ρ := Bicategory.Context) e
  match ctx? with
  | some _ =>
    return .bicategory
  | none =>
    let ctx? ← BicategoryLike.mkContext? (ρ := Monoidal.Context) e
    match ctx? with
    | some _ =>
      return .monoidal
    | none =>
      return .none

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

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

Разделы

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

Аффилиация

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