From 55db56f80de79c73a28f884ceb87ff117f127ebc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Dec 2021 10:34:40 -0800
Subject: [PATCH] feat: add `noncomputable section` parser

---
 src/Lean/Elab/Command.lean   | 2 ++
 src/Lean/Parser/Command.lean | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 5cf8ce8cdd..707fac3bf0 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -26,6 +26,8 @@ structure Scope where
   varDecls      : Array Syntax := #[]
   /-- Globally unique internal identifiers for the `varDecls` -/
   varUIds       : Array Name := #[]
+  /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
+  isNoncomputable : Bool := false
   deriving Inhabited
 
 structure State where
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 299c5bb4b8..f0fc15f1aa 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -93,6 +93,7 @@ def «structure»          := leading_parser
 @[builtinCommandParser] def declaration := leading_parser
 declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 @[builtinCommandParser] def «deriving»     := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
+@[builtinCommandParser] def noncomputableSection := leading_parser "noncomputable " >> "section " >> optional ident
 @[builtinCommandParser] def «section»      := leading_parser "section " >> optional ident
 @[builtinCommandParser] def «namespace»    := leading_parser "namespace " >> ident
 @[builtinCommandParser] def «end»          := leading_parser "end " >> optional ident