feat(init/lean/parser/macro): global names can be overloaded

This commit is contained in:
Sebastian Ullrich 2018-05-29 16:42:52 +02:00
parent a7760631dc
commit c4d7eb7949

View file

@ -34,8 +34,8 @@ def run' {r σ α} (cfg : r) (st : σ): parse_m r σ α → except string α :=
end parse_m
structure resolved :=
-- local or global
(decl : syntax_id ⊕ name)
-- local or (overloaded) global
(decl : syntax_id ⊕ list name)
/- prefix of the reference that corresponds to the decl. All trailing name components
are field accesses. -/
(«prefix» : name)