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

chore: remove bootstrapping workaround

Browse source
This commit is contained in:
Leonardo de Moura 2024-03-13 20:46:04 -07:00 • committed by Leonardo de Moura
parent 653eb5f66e
commit 9ee1ff2435
3 changed files with 1 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/Declaration.lean
View file

@ -43,7 +43,6 @@ private def isNamedDef (stx : Syntax) : Bool :=
let k := decl.getKind
k == ``Lean.Parser.Command.abbrev ||
k == ``Lean.Parser.Command.definition ||
k == ``Lean.Parser.Command.def || -- TODO: delete
k == ``Lean.Parser.Command.theorem ||
k == ``Lean.Parser.Command.opaque ||
k == ``Lean.Parser.Command.axiom ||

3
src/Lean/Elab/DefView.lean
View file

@ -143,7 +143,6 @@ def isDefLike (stx : Syntax) : Bool :=
let declKind := stx.getKind
declKind == ``Parser.Command.abbrev ||
declKind == ``Parser.Command.definition ||
declKind == ``Parser.Command.def || -- TODO: delete
declKind == ``Parser.Command.theorem ||
declKind == ``Parser.Command.opaque ||
declKind == ``Parser.Command.instance ||
@ -155,8 +154,6 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
return mkDefViewOfAbbrev modifiers stx
else if declKind == ``Parser.Command.definition then
return mkDefViewOfDef modifiers stx
else if declKind == ``Parser.Command.def then -- TODO: delete
return mkDefViewOfDef modifiers stx
else if declKind == ``Parser.Command.theorem then
return mkDefViewOfTheorem modifiers stx
else if declKind == ``Parser.Command.opaque then

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

@ -116,8 +116,6 @@ def optDefDeriving :=
optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
def definition := leading_parser
"def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
def «def» := leading_parser -- TODO: delete
"def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
def «theorem» := leading_parser
"theorem " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> declVal
def «opaque» := leading_parser
@ -200,7 +198,7 @@ def «structure» := leading_parser
optDeriving
@[builtin_command_parser] def declaration := leading_parser
declModifiers false >>
(«abbrev» <|> definition <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
(«abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
«inductive» <|> classInductive <|> «structure»)
@[builtin_command_parser] def «deriving» := leading_parser
"deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "