vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

suggestions missing

Open kckennylau opened this issue 5 years ago • 0 comments

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)

kckennylau avatar Jul 21 '20 11:07 kckennylau