Significant speedups in Construction/Comma/Isomorphism.v, thanks to Columbus240

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

Significant speedups in Construction/Comma/Isomorphism.v, thanks to Columbus240 #52

Closed jwiegley closed 2 years ago

jwiegley commented 2 years ago

@Columbus240 There's just one file with changes left to make into a PR, but I want to be sure the benefit is worth the size increase in the proof scripts...