vscode-lean
vscode-lean copied to clipboard
suggestions missing
Pressing Ctrl+Space (Cmd+Space for Mac) at the end of #check foo.bar gives no suggestions, instead of foo.bar, as it should.
class foo (α : Type) : Type :=
(bar : ℕ)
#check foo.bar
(https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/suggestions.20missing)