Skip to content

Commit

Permalink
fix: invalid namespace completions
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Sep 12, 2024
1 parent adfd6c0 commit 32854c1
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion src/Lean/Environment.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1016,7 +1016,15 @@ private def registerNamePrefixes : Environment → Name → Environment

@[export lean_environment_add]
private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
let env := registerNamePrefixes env cinfo.name
let name := cinfo.name
let env := match name with
| .str _ s =>
if s.get 0 == '_' then
-- Do not register namespaces that only contain internal declarations.
env
else
registerNamePrefixes env name
| _ => env
env.addAux cinfo

@[export lean_display_stats]
Expand Down

0 comments on commit 32854c1

Please sign in to comment.