mor₁OfExpr

Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.mor₁OfExpr

Lean4

/-- Construct a `Mor₁` expression from a Lean expression. -/
partial def mor₁OfExpr (e : Expr) : BicategoryM Mor₁ := do
  if let some f := (← get).cache.find? e then
    return f
  let f ←
    if let some a← id₁? e then
      MonadMor₁.id₁M a
    else if let some (f, g)← comp? e then
      MonadMor₁.comp₁M (← mor₁OfExpr f.e) (← mor₁OfExpr g.e)
    else
      return Mor₁.of ⟨e, ⟨← srcExpr e⟩, ⟨← tgtExpr e⟩⟩
  modify fun s => { s with cache := s.cache.insert e f }
  return f

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

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

Разделы

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

Аффилиация

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