@Kha I implemented the following approach:
- Error if user tries to revert `auxDecl`.
- Clear any `auxDecl` that depends on variables being reverted by the user.
@Kha This commit adds auto bound implicits to constructors.
I was excited until I tried to define the `Bigstep` type again without
`autoBoundImplicitLocal`, and found small typos.
Example, I had
```
| ifTrue : eval σ₁ b = true → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t₁ + 1)
```
where `t₁` should be `t`, but the declaration was accepted. I am
wondering whether Isabelle performs some kind of sanity checking,
and/or enforces rules such as: auto-bound implicits may only be
introduced by hypotheses.
Note that this is not an issue for definitions, because the body of
the definition will probably not type check when we have this kind of
typo in the header.
Anyway, I am putting the experiment in this branch for now.
That being said, the `Bigstep` declaration is way nicer with
`autoBoundImplicitLocal`s.
Another option is to add a new option `ctorAutoBoundImplicitLocal`
that is false by default, and activates auto implicit locals for
constructors when set to true.
This issue produced a nested inductive datatype that could not be
handled by the kernel. See new test.
Without the fix, the inductive declaration contained the term
```
((fun α {n : Nat} (t : Vec α n) => ...) Expr n x)
```
The nested occurrence `Vec Expr n` only becomes explicit after
beta-reduction.
This issue exposed two bugs at `Structural.lean`
1- `getFixedPrefix` was using structural equality to detected fixed
arguments. We should use definitional equality.
2- The `replaceFVars` was broken. We should use `instantiateForall` instead.
We now (try to) postpone `match ... with` elaboration when pattern
variables and patterns still contain metavariables before invoking `mkMatcher`.
This improvement makes sure we can elaborate an example submitted by
Daniel Selsam.
Remark: this update may create performance problems since we
backtrack `elabMatchTypeAndDiscrs` and `elabMatchAltView`.
We hope this is not a problem in practice since we use the "quick-check"
`waitExpectedTypeAndDiscrs`. Recall that we could compile Lean
without this commit. So, it suggests cases where we need to postpone
after `elabMatchAltView` are rare.
