e2983e44ef
Because of the last-added-tried-first rule for macros, all the special purpose `decreasing_trivial` rules are tried for most recursive definitions out there, and because they use `apply` and `assumption` with default transparency may cause some definitoins to be unfolded over and over again. A quick test with one of the functions in the leansat project shows that elaboration time goes down from 600ms to 375ms when using ``` decreasing_by all_goals decreasing_with with_reducible decreasing_trivial ``` instead of ``` decreasing_by all_goals decreasing_with decreasing_trivial ``` This change uses `with_reducible` in most of these macros. This means that these tactics will no longer work when the relations/definitions they look for is hidden behind a definition. This affected in particular `Array.sizeOf_get`, which now has a companion `sizeOf_getElem`. In addition, there were three tactics using `apply` to apply Nat-related lemmas that we now expect `omega` to solve. We still need them when building `Init` modules that don’t have access to `omega`, but they now live in `decreasing_trivial_pre_omega`, meant to be only used internally. |
||
|---|---|---|
| .. | ||
| Nat | ||
| Basic.lean | ||
| Main.lean | ||
| Nat.lean | ||
| Simp.lean | ||
| Solver.lean | ||