For example, `mkFreshExprMVar none MetavarKind.synthetic` should
create a fresh synthetic metavariable `?m` with type `?t` where `?t`
is a fresh natural metavariable. If users want a synthetic
metavariable `?t`, then it must create it themselves.
@Kha I am also tracking `currNamespace` and `openDecls`.
BTW, I also tried an experiment where I added `currNamespace` and
`openDecls` to `Meta.Context`, but it looked weird. This information
is only needed in the elaborator and pretty printer.
The `PPContext` object should contain everything you need. You
can put `currNamespace` and `openDecls` in the `Delaborator.Context`.
The `matchType` created by the macro is bad for dependent pattern
matching. The `tst8` and `tst9` at `matchTac` failed to be elaborated
when using the macro.
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
Eq.trans this (by assumption)
```
It had to be fixed because we have code that needs to be compiled with
the old frontend, and the hacks we used to workaround this issue are
incompatible with the new frontend.
@Kha this is a little bit ugly. As in Lean3, the notation `{ }` is
overloaded. It can be `HasEmptyc.emptyc` or the empty structure.
Moreover, if we have an instance `HasEmptyc A` for a structure `A`,
then `{ }` is notation for `HasEmptyc.emptyc`. I am not very happy
about this, but it seems users use this feature. It is even used in
our own Lean4 code base :)
BTW, I will try a different alternative later.
First, move the notation `{ }` as a proper parser for `emptyc`.
Then, make sure the elaborator throws an error when
`{ }` is ambiguous. That is, `{}` can be elaborated as the empty
structure `A` and there is an `HasEmptyc A` instance.
Example:
```
structure A :=
(x : Nat := 0)
instance : HasEmptyc A :=
⟨{ x := 10 }⟩
```
The main issue here is that the support for choice+postpone is
currently broken.
@Kha it now uses the same precedence of `fun`.
The main motivation is to allow us to write `@by { ... }` instead of
`@(by { ... })`.
BTW, I am considering disabling implicit lambdas for `by ...` expressions.
It is automatically "intro"ducing the implicit variables without
giving an opportunity for users to pick their names.
@Kha This is a first attempt to improve the error message for examples
like the one Andrew Kent posted on Zulip.
I created a simpler example using "vectors".
Given
```
inductive Foo
| mk₁ (x y z w : Nat)
| mk₂ (x y z w : Nat)
```
We can now write
```
def Foo.z : Foo → Nat
| mk₁ (z := z) .. => z
| mk₂ (z := z) .. => z
```
instead of
```
def Foo.z : Foo → Nat
| mk₁ _ _ z _ => z
| mk₂ _ _ z _ => z
```
cc @Kha
