Gabriel Ebner

> For what it's worth, `rust-analyzer` has a much more efficient way of introduce `match` compared to typing `{! x !}`: Here are some previous discussions we've had on abusing...

> This is awesome! Could you comment on whether there is a clear path to implementing Daniel's [proposal](https://github.com/leanprover/lean4/issues/400#issuecomment-819752356) later as well? Is it possible to implement something like Daniel suggested...

> It would either need server support so that we don't have to eagerly `toInteractive` the entire trace, or we could send just a "trace outline" containing only the classes...

> BTW, the PR is currently marked as a draft, is something missing? I wanted some discussion on the RPC API first (see exchange with Wojciech). There's also plenty of...

Thinking about the search API issue a bit more, I believe that all searching should happen server-side. This is great because: - It also works on the command-line. - Filters...

> It looks like this could also serve as the basis for a metaprogram that essentially tests a trace against a spec, right? The idea here is that I'd like...

I've changed the serialization of `trace` to an object to make easier to extend in the future. See comment above about server-side search.

I think go-to-references only works with `lake serve` iirc.

I'm not sure what the takeaway here is: 1. Never use nested ``. 2. Add antiquotations for ``. 3. Add antiquotations for symbols. 4. Add a `leading_parser` to `def binderIdent`.

> say whenever `str` is not used in a sequence More conservatively, we could also say whenever `str` is used directly in a ``. The difference between the heuristics would...