stringEqM?

Mathlib.Tactic.Widget.StringDiagram

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

Lean4

/-- Given an equality between 2-morphisms, return a string diagram of the LHS and RHS.
Otherwise `none`. -/
def stringEqM? (e : Expr) : MetaM (Option Html) := do
  let e ← whnfR <| ← instantiateMVars e
  let some (_, lhs, rhs) := e.eq? |
    return none
  let some lhs ← stringM? lhs |
    return none
  let some rhs ← stringM? rhs |
    return none
  return some <| mkEqHtml lhs rhs

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

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

Разделы

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

Аффилиация

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