This module defines tactic/meta infrastructure for displaying commutative diagrams in the infoview.

@[inline]

def Lean.Expr.app7? (e : Lean.Expr) (fName : Lean.Name) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

If the expression is a function application of fName with 7 arguments, return those arguments. Otherwise return none.

Equations

• One or more equations did not get rendered due to their size.

Metaprogramming utilities for breaking down category theory expressions

def Mathlib.Tactic.Widget.homType? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Given a Hom type α ⟶ β, return (α, β). Otherwise none.

Equations

• Mathlib.Tactic.Widget.homType? e = match Lean.Expr.app4? e `Quiver.Hom with | some (fst, fst_1, A, B) => pure (A, B) | x => none

def Mathlib.Tactic.Widget.homComp? (f : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Given composed homs g ≫ h, return (g, h). Otherwise none.

Equations

• Mathlib.Tactic.Widget.homComp? f = match Lean.Expr.app7? f `CategoryTheory.CategoryStruct.comp with | some (fst, fst_1, fst_2, fst_3, fst_4, f, g) => pure (f, g) | x => none

@[inline, reducible]

abbrev Mathlib.Tactic.Widget.ExprEmbeds : Type

Expressions to display as labels in a diagram.

Equations

• Mathlib.Tactic.Widget.ExprEmbeds = Array (String × Lean.Expr)

Widget for general commutative diagrams

def Mathlib.Tactic.Widget.mkCommDiag (sub : String) (embeds : Mathlib.Tactic.Widget.ExprEmbeds) : Lean.MetaM ProofWidgets.Html

Construct a commutative diagram from a Penrose substance program and expressions embeds to display as labels in the diagram.

Equations

• One or more equations did not get rendered due to their size.

Commutative triangles

def Mathlib.Tactic.Widget.subTriangle : String

Triangle with homs = [f,g,h] and objs = [A,B,C]

A f B
  h g
    C

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Widget.commTriangleM? (e : Lean.Expr) : Lean.MetaM (Option ProofWidgets.Html)

Given a commutative triangle f ≫ g = h or e ≡ h = f ≫ g, return a triangle diagram. Otherwise none.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Widget.commutativeTrianglePresenter : ProofWidgets.ExprPresenter

Equations

• One or more equations did not get rendered due to their size.

Commutative squares

def Mathlib.Tactic.Widget.subSquare : String

Square with homs = [f,g,h,i] and objs = [A,B,C,D]

A f B
i   g
D h C

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Widget.commSquareM? (e : Lean.Expr) : Lean.MetaM (Option ProofWidgets.Html)

Given a commutative square f ≫ g = i ≫ h, return a square diagram. Otherwise none.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Widget.commutativeSquarePresenter : ProofWidgets.ExprPresenter

Equations

• One or more equations did not get rendered due to their size.