search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
744 stars 68 forks source link

Speed up Structure/Monoidal/Internal/Product.v, thanks to Columbus240 #56

Closed jwiegley closed 2 years ago

jwiegley commented 2 years ago

This is being achieved in a more manual way, but it offers a great basis for improving tactics later to see if the fully automated solutions (which are given by the [solveit] tactic) can be made comparable in speed.

jwiegley commented 2 years ago

@Columbus240 All of your recent changes are now committed, thank you again!