Def Mathlib.Tactic.BicategoryCoherence.exception'

Modification history

2026-06-16 21:10

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

chore: avoid `meta`-importing math files (#40671) …

Deleted Mathlib.Tactic.BicategoryCoherence.exception'View on Github →

2023-06-07 03:09

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

feat: port CategoryTheory.Bicategory.CoherenceTactic (#4610)

Added Mathlib.Tactic.BicategoryCoherence.exception'View on Github →