Commit 2020-04-16 11:10 ec800611
View on Github →refactor(analysis/asymptotics): make is_o irreducible (#2416)
is_o is currently not irreducible. Since it is a complicated type, Lean can have trouble checking if two types with is_o are defeq or not, leading to timeouts as described in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/undergraduate.20calculus/near/193776607
This PR makes is_o irreducible.