max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/elaborator): resolve idents after 'attribute'

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-21 17:47:17 +01:00
parent 280dc4e8d8
commit 53d9cb5358
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/elaborator.lean
View file

@ -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 :=