From 53d9cb5358e18926d2c2b9ecee4e296c6b3b19bc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Jan 2019 17:47:17 +0100 Subject: [PATCH] fix(library/init/lean/elaborator): resolve idents after 'attribute' --- library/init/lean/elaborator.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index b0cf9f11cc..251c8c89f2 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -788,7 +788,11 @@ def attribute.elaborate : elaborator := let mdata := kvmap.set_name {} `command `attribute, let mdata := mdata.set_bool `local $ attr.local.is_some, attrs ← attrs_to_pexpr attr.attrs, - let ids := expr.mk_capp `_ $ attr.ids.map $ λ id, expr.const (mangle_ident id) [], + ids ← attr.ids.mmap (λ id, match id.preresolved with + | [] := error (syntax.ident id) $ "unknown identifier '" ++ to_string id.val ++ "'" + | [c] := pure $ expr.const c [] + | _ := error (syntax.ident id) "invalid 'attribute' command, identifier is ambiguous"), + let ids := expr.mk_capp `_ ids, old_elab_command stx $ expr.mdata mdata $ expr.app attrs ids def check.elaborate : elaborator :=