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

feat: add opaque command

Browse source 
It will replace the `constant` command. See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20is.20.60opaque.60.3F/near/284926171
This commit is contained in:
Leonardo de Moura 2022-06-14 16:22:36 -07:00
parent d7cb93e9e4
commit 05778565ab
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -71,6 +71,7 @@ def optDefDeriving := optional (atomic ("deriving " >> notSymbol "instance") >
def «def» := leading_parser "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
def «theorem» := leading_parser "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
def «constant» := leading_parser "constant " >> declId >> ppIndent declSig >> optional declValSimple
def «opaque» := leading_parser "opaque " >> declId >> ppIndent declSig >> optional declValSimple
/- As `declSig` starts with a space, "instance" does not need a trailing space if we put `ppSpace` in the optional fragments. -/
def «instance» := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
def «axiom» := leading_parser "axiom " >> declId >> ppIndent declSig
@ -95,7 +96,7 @@ def «structure» := leading_parser
>> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
>> optDeriving
@[builtinCommandParser] def declaration := leading_parser
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «opaque» <|> «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