* 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.
The goal is to address the regression
```
example : (0 : Nat) + 0 = 0 :=
show 0 + 0 = 0 from rfl
```
introduced by fedf235cba
Note that we should only *try to* unify the types. Otherwise, we would
produce another regression.
```
example : Int :=
show Nat from 0
```
cc @kha
In Lean 4, we have support for typing constraints of the form
```
(?m ...).1 =?= v
```
where the type of `?m ...` is a structure with a single field.
This kind of constraint is reduced to `?m ... =?= ⟨v⟩`
This feature is implemented by the function `isDefEqSingleton`.
As far as I remember, Lean 3 does not implement this feature.
This commit disables this feature if the structure is a class.
The goal is to avoid the generation of counterintuitive instances by
typing inference.
For example, in the example at issue #2011, the following weird
instance was being generated for `Zero (f x)`
```
(@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝)
```
where `inst✝¹` is the local instance `[∀ i, Zero (f i)]`
Note that this instance is definitinally equal to the expected nicer
instance `inst✝¹ x✝`.
However, the nasty instance trigger nasty unification higher order
constraints later.
Note that a few tests broke because different error messages were
produced. The new error messages seem better. I do not expect this
change to affect Mathlib4 since Lean 3 does not have this feature.
