d51a5b920d
This PR modifies macros, which implement non-atomic definitions and ```$cmd1 in $cmd2``` syntax. These macros involve implicit scopes, introduced through ```section``` and ```namespace``` commands. Since sections or namespaces are designed to delimit local attributes, this has led to unintuitive behaviour when applying local attributes to definitions appearing in the above-mentioned contexts. This has been causing the following examples to fail: ```lean4 axiom A : Prop namespace ex1 open Nat in @[local simp] axiom a : A ↔ True example : A := by simp end ex1 namespace ex2 @[local simp] axiom Foo.a : A ↔ True example : A := by simp end ex2 ``` This PR adds an internal-only piece of syntax, ```InternalSyntax.end_local_scope```, that influences the ```ScopedEnvExtension.addLocalEntry``` used in implementing local attributes, to avoid delimiting local entries in the current scope. This command is used in the above-mentioned macros. Closes [#9445](https://github.com/leanprover/lean4/issues/9445). --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||