Ed Ayers

not yet; got to write a `Float → JsonNumber` function.

Ok I wrote a `Float → JsonNumber` function but it goes via `toString : Float → String` for now.

I am keen to work on this

I can think of two ways of implementing this: 1. VSCode's goal view component intercepts rendering of tagged text and highlights subexpressions that have changed since the last render. React...

@gebner > 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 location details...

@leodemoura > Does it make sense to integrate the "Try this" feature with this one? For example, we could show hints by default in the info view as a form...

For (4), could the code actions be triggered by an `_` that could not be inferred?

> Thanks! So these are four cases and not an arbitrary-length list. In that case I think it would be better to make an inductive for it. Yeah it was...

> Now I have a new question: how do you specify the tactic state to the `queryContextualSuggestions`? Is it "whatever `getInteractiveGoals` returns for the position"? There can be more than...

@gebner > the current SubExpr.Pos JSON encoding won't roundtrip through the vscode that's a good spot, I'm currently in the process of writing a [library for `SubExpr.Pos`](https://github.com/EdAyers/lean4/blob/5b2fac8bec62530831aea64d64724f140ff5b933/src/Lean/SubExpr.lean#L29), I can change...