Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.
Closes#1045
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.
We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.
I tried a few benchmarks and did not notice a significant difference.
cc @kha @gebner
fixes#1051
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.
The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
| stop : HasType 0 (ty :: ctx) ty
| pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty
inductive Sublist : List α → List α → Prop
| slnil : Sublist [] []
| cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
| cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
inductive Lst : Type u → Type u
| nil : Lst α
| cons : α → Lst α → Lst α
```
TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.
TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
TODO: convert fixed indices to parameters. Motivation: types such as
```lean
inductive Foo : List α → Type
| mk : Foo []
```
Users should not need to write
```lean
inductive Foo {α} : List α → Type
| mk : Foo []
```
