From aadf2eb5c1dfe83219339e70a61336797cbb0d8a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 6 Jan 2019 18:18:10 +0100 Subject: [PATCH] fix(library/init/lean/elaborator): `resolve_global`: add missing name part, append root and `open` resolutions --- library/init/lean/elaborator.lean | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 6c59b1dd6a..2c89ec300b 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -688,22 +688,22 @@ def resolve_global : name → elaborator_m (list name) | n := do st ← get, - -- check surrounding namespaces + -- check surrounding namespaces first -- TODO: check for `protected` match st.local_state.ns_stack.filter (λ ns, st.env.contains (ns ++ n)) with - | n'::_ := pure [n'] -- prefer innermost namespace - | _ := do + | ns::_ := pure [ns ++ n] -- prefer innermost namespace + | _ := pure $ -- check environment directly - let unrooted := n.replace_prefix `_root_ name.anonymous, - match st.env.contains unrooted with - | tt := pure [unrooted] - | _ := do - + (let unrooted := n.replace_prefix `_root_ name.anonymous in + match st.env.contains unrooted with + | tt := [unrooted] + | _ := []) + ++ -- check opened namespaces -- TODO: `hiding`, `as`, `export` - let ns' := st.local_state.open_decls.map (λ od, od.id.val ++ n), - pure $ ns'.filter (λ n', st.env.contains n') + (let ns' := st.local_state.open_decls.map (λ od, od.id.val ++ n) in + ns'.filter (λ n', st.env.contains n')) -- TODO: projection notation