@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.
1731962ea9