@Kha, Jason's example on issue #337 suggests that injecting
implicit-lambdas while elaborating patterns is problematic.
The elaborator was injecting `fun {Γ} =>` before the
pattern variable `ftm`.
So, I disabled the implicit-lambda during pattern elaboration. I
didn't find an example where it would be useful.
see #337
cc @JasonGross
closes#318
Like Lean 3, we are doing it only for theorems.
@Kha, we talked about doing it for definitions too, it sounded like a
good idea, and it would make the system's behavior more uniform, but
unfortunately it creates too many problems. There are so many trivial
cases where it breaks. Here are some examples.
1- Definitions that take multiple bundled structures
```
def foo (s1 : Group) (s2 : CommRing) ...
```
They are universe polymorphic, and the different structures must be in
the same universe, but we don't know it when we elaborate the header,
that is, we need to elaborate the body.
An extreme case is `PUnit` occurring in the header. It is universe
polymorphic, but we only lear the constraints on this universe after
we elaborate the body.
2- All files containing unification hints broke.
Again, there are universe constraints on the header that we only learn
after we elaborate the body.
3- Many `CoeSort` and `CoeFun` examples broke.
Example:
```
structure Group :=
(carrier : Type u) (mul : carrier → carrier → carrier) (one : carrier)
instance GroupToType : CoeSort Group (Type u) :=
CoeSort.mk (fun g => g.carrier)
```
We would have to write
```
instance GroupToType : CoeSort Group.{u} (Type u) :=
CoeSort.mk (fun g => g.carrier)
```
We would have to provide universe level parameters manually in this
kind of instance. I think it would be too annoying.
@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.
