You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Fixes#4455, fixes#4705, fixes#5219
Also fixes a minor bug where a dot in brackets would report incorrect
completions instead of no completions.
---------
Co-authored-by: Sebastian Ullrich <[email protected]>
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
When I type
a
in the lambda, LSP only suggests the symbols in the namespace ofList
, not global symbols.Context
Zulip discussion
Steps to Reproduce
a
in the lambda.Expected behavior:
Show global symbols, including
aaaaa
.Actual behavior: [Clear and concise description of what actually happens]
Only show symbols in
List
namespace.Versions
4.9.0-rc1
Additional Information
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: