The check_compositions tactic, which checks the typing of categorical compositions in the goal, reporting discrepancies at "instances and reducible" transparency.

Reports from this tactic do not necessarily indicate a problem, although typically simp should reduce rather than increase the reported discrepancies.

check_compositions may be useful in diagnosing uses of erw in the category theory library.

def Mathlib.Tactic.CheckCompositions.forEachComposition (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Unit) : Lean.MetaM Unit

Find appearances of CategoryStruct.comp C inst X Y Z f g, and apply f to each.

Equations

• Mathlib.Tactic.CheckCompositions.forEachComposition e f = e.forEach fun (e : Lean.Expr) => if e.isAppOfArity `CategoryTheory.CategoryStruct.comp 7 = true then f e else pure ()

def Mathlib.Tactic.CheckCompositions.checkComposition (e : Lean.Expr) : Lean.MetaM Unit

Given a composition CategoryStruct.comp _ _ X Y Z f g, infer the types of f and g and check whether their sources and targets agree, at "instances and reducible" transparency, with X, Y, and Z, reporting any discrepancies.

Equations

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

def Mathlib.Tactic.CheckCompositions.checkCompositions (e : Lean.Expr) : Lean.MetaM Unit

Check the typing of categorical compositions in an expression.

Equations

• Mathlib.Tactic.CheckCompositions.checkCompositions e = Mathlib.Tactic.CheckCompositions.forEachComposition e Mathlib.Tactic.CheckCompositions.checkComposition

def Mathlib.Tactic.CheckCompositions.checkCompositionsTac : Lean.Elab.Tactic.TacticM Unit

Check the typing of categorical compositions in the goal.

Equations

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

def Mathlib.Tactic.CheckCompositions.tacticCheck_compositions : Lean.ParserDescr

For each composition f ≫ g in the goal, which internally is represented as CategoryStruct.comp C inst X Y Z f g, infer the types of f and g and check whether their sources and targets agree with X, Y, and Z at "instances and reducible" transparency, reporting any discrepancies.

Equations

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