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

@[inline]

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

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

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.

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

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

@[reducible, inline]

abbrev Mathlib.Tactic.Widget.ExprEmbeds : Type

Expressions to display as labels in a diagram.

Widget for general commutative diagrams

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

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

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

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.

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

Presenter for a commutative triangle

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

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.

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

Presenter for a commutative square