irreducible definitions

Stream: mathlib4

[Yury G. Kudryashov]

Should we make more definitions in Mathlib irreducible? I'm working on some code about Lists, and a theorem was extremely slow (15s for a few simp calls). It turns out that Lean tried to unfold List.modify 50K times, because some definitions in the file weren't irreducible. I wonder if we have more performance hits because of Lean trying to unfold definitions.

E.g., can we see which definitions get unfolded most in unsuccessful isDefEq calls?

[Sebastian Ullrich]

diagnostics should give you grand totals, does that help?

[Yury G. Kudryashov]

Per file or over the whole repo?

[Sebastian Ullrich]

Per declaration

[Yury G. Kudryashov]

I'll see if I can figure out how to sum over the repo after I come back home (flying to a week in the office in a few hours, will have very little time for Mathlib there).