stringMorOrEqM?

Mathlib.Tactic.Widget.StringDiagram

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

Lean4

/-- Given an 2-morphism or equality between 2-morphisms, return a string diagram.
Otherwise `none`. -/
def stringMorOrEqM? (e : Expr) : MetaM (Option Html) := do
  forallTelescopeReducing (← whnfR <| ← inferType e) fun xs a => do
      if let some html← stringM? (mkAppN e xs) then
        return some html
      else if let some html← stringEqM? a then
        return some html
      else
        return none

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

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

Разделы

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

Аффилиация

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