fix: open .. hinding .. should activate scoped attributes
This commit is contained in:
parent
e369c3beb6
commit
5a8f9ace72
2 changed files with 14 additions and 0 deletions
|
|
@ -76,6 +76,7 @@ def elabOpenDecl [MonadResolveName m] (stx : TSyntax ``Parser.Command.openDecl)
|
|||
addOpenDecl (OpenDecl.explicit idStx.getId declName)
|
||||
| `(Parser.Command.openDecl| $ns hiding $ids*) =>
|
||||
let ns ← resolveUniqueNamespace ns
|
||||
activateScoped ns
|
||||
for id in ids do
|
||||
let _ ← resolveId ns id
|
||||
let ids := ids.map (·.getId) |>.toList
|
||||
|
|
|
|||
13
tests/lean/run/scopedHindingIssue.lean
Normal file
13
tests/lean/run/scopedHindingIssue.lean
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
namespace Foo
|
||||
|
||||
def x := 10
|
||||
|
||||
scoped macro "~0~" : term => `(0)
|
||||
|
||||
#check ~0~
|
||||
|
||||
end Foo
|
||||
|
||||
open Foo hiding x -- must open scoped notation and attributes too
|
||||
|
||||
#check ~0~
|
||||
Loading…
Add table
Reference in a new issue