Gabriel Ebner

> This would require enabling HTML in hovers in the client More importantly, it also requires the client to support the HTML we use in the hovers. So the server...

> Because we want a quotation pattern in a semantic transformation, e.g. a macro, that used fun to still match if the user wrote λ. Note that we only have...

As requested by Wojciech, I'm reposting here what I wrote about interactive traces on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Expandable.20trace.20API/near/257867137). We should make all nested traces collapsible, and not just the nodes added using `traceCtx`....

> > `withNestedTraces (cls : Name) (msg : MessageData) (k : m α) (collapsed := false) : m α` > > Is the intended usage the same as `traceCtx`? That...

> I'm not sure what to think of the `quote SourceInfo` change, compared to directly moving to `quote [MonadQuotation m] : A -> m A` (and ditching all the `Unhygiene.run`s)....

Nice proposal! It's great to see progress on suggestions. Can you please explain how the location is computed (that the client passes to `queryContextualSuggestions`)? This part seems to be completely...

> > Can you please explain how the location is computed (that the client passes to `queryContextualSuggestions`)? This part seems to be completely missing. > > Added to RFC in...

> Does it make sense to integrate the "Try this" feature with this one? Maybe it's helpful to categorize the various kinds of useful code insertion features that we want...

> For (4), could the code actions be triggered by an _ that could not be inferred? Yes, that's how it worked in Lean 3 and that seems like a...

BTW, the current `SubExpr.Pos` JSON encoding won't roundtrip through the vscode LSP library. (Since the default javascript JSON parser converts every number to a float.) From what I can tell...