fix: resolveGlobalName for atomic references to private names

This commit is contained in:
Leonardo de Moura 2020-07-23 14:58:19 -07:00
parent ea5eed7964
commit e4865f5aad
2 changed files with 9 additions and 0 deletions

View file

@ -88,6 +88,8 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li
| some newId => [(newId, projs)]
| none =>
let resolvedIds := if env.contains id then [id] else [];
let idPrv := mkPrivateName env id;
let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds;
let resolvedIds := resolveOpenDecls env id openDecls resolvedIds;
let resolvedIds := getAliases env id ++ resolvedIds;
match resolvedIds with

7
tests/lean/run/prv.lean Normal file
View file

@ -0,0 +1,7 @@
new_frontend
private def x := 10
#check _root_.x
#check x
#eval x + 1