diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index d18429e42a..3081946eb8 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -87,7 +87,7 @@ private def checkEndHeader : Name → List Scope → Option Name @[builtin_command_elab «section»] def elabSection : CommandElab := fun stx => do match stx with - | `(Parser.Command.section| $[public%$publicTk]? $[@[expose%$expTk]]? $[noncomputable%$ncTk]? section $(header?)?) => + | `(Parser.Command.section| $[@[expose%$expTk]]? $[public%$publicTk]? $[noncomputable%$ncTk]? section $(header?)?) => -- TODO: allow more attributes? let attrs ← if expTk.isSome then pure [← `(Parser.Term.attrInstance| expose)] diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 6ee413dc7e..8086a4282b 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -247,8 +247,8 @@ def «structure» := leading_parser @[builtin_command_parser] def «deriving» := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", " def sectionHeader := leading_parser - optional ("public ") >> optional ("@[" >> nonReservedSymbol "expose" >> "] ") >> + optional ("public ") >> optional ("noncomputable ") /-- A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`