mathlib
8d199395 - feat(*): make `int.le` irreducible (#4474)

Commit
5 years ago
feat(*): make `int.le` irreducible (#4474) There's very rarely a reason to unfold `int.le` and it can create trouble: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deep.20recursion.20was.20detected.20at.20'replace' Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading