mathlib
86ee6689 - fix(algebra/category/Module): speedup (#16371)

Commit
3 years ago
fix(algebra/category/Module): speedup (#16371) This change makes `map'` go from using 95,000+ heartbeats (that is, `lean --make -T95000` fails locally) to using less than 25,000. With `set_option pp.all true`, the output of `#print map'` is the same before and after this change, but note that this is a `def` so perhaps using the `apply` tactic is not appropriate.
Author
Parents
Loading