Gabriel Ebner

I think these could prove to be fairly controversial. You automatically get a lot of text when you type `structure`. I don't see an easy way to avoid the snippets...

Ok, so I've tried them out a bit. - They are not triggered automatically unless you explicitly select them in the dropdown. This is good. - The `structure` snippet does...

Yeah, I am well aware that this can happen. I've been fixing them whenever they become an issue. Unfortunately it seems to be impossible to tell vscode to stop the...

This is a bug in core Lean, the vscode extension is just printing what it gets from the server. And I fear it will stay this way for eternity. Lean...

@mjbvz We have been using a horrible workaround for https://github.com/microsoft/vscode/issues/89038, at the moment we are running our own web server on localhost to avoid `vscode-resource:` uris. The fix is coming...

> Tooltips for declarations / names in the infoview seem like they would be much harder. We could try to extend the support we have in place for the documentation...

I think you need to open a Lean file first.

> My current idea is that we would show the preview in the infoview whenever the cursor is inside a docstring I like this idea! > We could find out...

See #100 and #101. cc @bryangingechen

We briefly talked about this last week. One possible solution could be to use total functions instead. That is: ```fstar let rec bigsum (m : nat) (n : nat) (f...