id₁?

Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.id₁?

Lean4

/-- Check that `e` is definitionally equal to `𝟙_ C`. -/
def id₁? (e : Expr) : MonoidalM (Option Obj) := do
  let ctx ← read
  match ctx.instMonoidal? with
  | some _monoidal =>
    do
      if ← withDefault <| isDefEq e (q(𝟙_ _) : Q($ctx.C)) then
        return some ⟨none⟩
      else
        return none
  | _ =>
    return none

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

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

Разделы

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

Аффилиация

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