Commit 2021-05-03 17:06 048240e8

chore(*): update to lean 3.30.0c (#7264) There's quite a bit of breakage from no longer reducing acc.rec so aggressively. That is, a well-founded definition like nat.factors will no longer reduce definitionally. Where you could write rfl before, you might now need to write by rw nat.factors or by simp [nat.factors]. A more inconvenient side-effect of this change is that dec_trivial becomes less powerful, since it also relies on the definitional reduction. For example nat.factors 1 = [] is no longer true by dec_trivial (or rfl). Often you can replace dec_trivial by simp or norm_num. For extremely simple definitions that only use well-founded relations of rank ω, you could consider rewriting them to use structural recursion on a fuel parameter instead. The functions nat.mod and nat.div in core have been rewritten in this way, please consult the corresponding Lean PR for details on the implementation.