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). |
||
|---|---|---|
| .. | ||
| BlaAttr.lean | ||
| MetaMid.lean | ||
| MetaUser.lean | ||
| Tst.lean | ||