max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add noncomputable section parser

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-13 10:34:40 -08:00
parent 0ade9ee39b
commit 55db56f80d
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Command.lean
View file

@ -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

1
src/Lean/Parser/Command.lean
View file

@ -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