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

source
@[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`.

Equations

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

Instances For

## Metaprogramming utilities for breaking down category theory expressions #

source
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 e.app4? `Quiver.Hom with | some (fst, fst_1, A, B) => pure (A, B) | x => none

Instances For

source
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 f.app7? `CategoryTheory.CategoryStruct.comp with | some (fst, fst_1, fst_2, fst_3, fst_4, f, g) => pure (f, g) | x => none

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.Widget.ExprEmbeds :
Type

Expressions to display as labels in a diagram.

Equations

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

Instances For

## Widget for general commutative diagrams #

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

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

Equations

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

Instances For

## Commutative triangles #

source
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.

Instances For

source
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.

Instances For

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

Presenter for a commutative triangle

Equations

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

Instances For

## Commutative squares #

source
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.

Instances For

source
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.

Instances For

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

Presenter for a commutative square

Equations

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

Instances For