*): use by apply to speed up elaboration (#7360)

Commit

5 years ago

chore(algebra/category/*): use by apply to speed up elaboration (#7360) A few more speed ups. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

a5cb13a6

mathlib 3093fd81 - chore(algebra/category/*): use by apply to speed up elaboration (#7360)

mathlib
3093fd81 - chore(algebra/category/*): use by apply to speed up elaboration (#7360)