This repository has been archived by the owner on Jun 26, 2024. It is now read-only.

suggestions missing #212

Open

kckennylau opened this issue Jul 21, 2020 · 0 comments

Contributor

kckennylau commented Jul 21, 2020

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)

The text was updated successfully, but these errors were encountered:

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.