e6dfdfdcee
This PR makes the elaborator reject `@[foo]` when the module that registers `foo` is not visibly imported into the current file but merely loaded as IR. Previously such uses silently elaborated but led to divergence of cmdline and server behavior and caused `lake shake --fix` to flip-flop on successive runs (#13599).
13 lines
230 B
Text
13 lines
230 B
Text
import UserAttr.Tst
|
|
import UserAttr.MetaUser
|
|
|
|
open Lean
|
|
|
|
def tst : MetaM Unit := do
|
|
let env ← getEnv
|
|
assert! (blaAttr.hasTag env `f)
|
|
assert! (blaAttr.hasTag env `g)
|
|
assert! !(blaAttr.hasTag env `id)
|
|
pure ()
|
|
|
|
#eval tst
|