The notation `a ∈ as` for Arrays was previously only defined with
`DecidableEq` on the elements, for (apparently) no good reason. This
drops this requirements (by using `a ∈ as.data`), and simplifies a bunch
of proofs by simply lifting the corresponding proof from lists.
Also, `sizeOf_lt_of_mem` was defined, but not set up to be picked up by
`decreasing_trivial` in the same way that the corresponding List lemma
was set up, so this adds the tactic setup.
The definition for `a ∈ as` is intentionally not defeq to `a ∈ as.data`
so that the termination tactics for Arrays don’t spuriously apply when
recursing through lists.
This commit also removes parameter `simpleReduce` from discrimination
trees, and take WHNF configuration options.
Reason: it is more dynamic now. For example, the simplifier
will be able to use different configurations for discrimination tree insertion
and retrieval. We need this feature to address issues #2669 and #2281
This commit also removes the dead Meta.Config field `zetaNonDep`.
* fix: `withCollectingNewGoalsFrom`
do not collect old goals
* fix: update occurs check
* test: fix test `run/492.lean`
* docs: add docstring to `elabTermWithHoles`
* test: `refineFiltersOldMVars`
* test: fix `expected.out` name
* test: fix `expected.out` filename and line numbers
* docs: use long ascii dash instead of em dash
Co-authored-by: Scott Morrison <scott@tqft.net>
* docs: fix long line, mention lean4#2502
* docs: a couple more long lines
* test: fix line numbers
---------
Co-authored-by: Scott Morrison <scott@tqft.net>
* remove |- as an alias for ⊢
* revert false positive |->
* fix docstring
* undo previous changes
* [unchecked] use suggestion
* next attempt
* add test
* feat: `funext` no arg tactic
Description of funext tactic includes behavior that is not implemented. This implements the behavior.
* fix
* feat: test new funext tactic
* use repeat for clarity of intent
Previously `decreasing_with` failed if `simp_wf` closes the goal on its
own. This can cause undesired regressions when new `simp` lemmas are
introduced.
Closes#2018.
