Commit 2024-09-09 01:17 be23ec97

View on Github →

chore(Tactic/CategoryTheory): fix meta code for monoidal categories (#15335) Several bug fixes and simple refactoring. The main changes:

  • Monoidal.lean: In structural?, the number of arguments in getAppFnArgs matching was wrong (I only considered explicit ones there). Infact, structural? is no longer needed since the matching is performed in eval. Now the monoidalCoherence is StructuralAtom, not Structural.
  • Coherence.lean: Unfolding MonoidalCoherence.hom by dsimp at the beginning of the coherence tactic.

Estimated changes