remove commented-out code

leanprover · Nov 22, 2024 · 44c24ea · 44c24ea
1 parent c9a9d90
commit 44c24ea
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
@@ -365,9 +365,6 @@ def structInstFieldBinder :=
     binderIdent <|> bracketedBinder
 def structInstField := ppGroup $ leading_parser
   structInstLVal >> many (checkColGt >> structInstFieldBinder) >> optional (atomic (" : " >> termParser >> notFollowedBy "}" "}")) >> optional (" := " >> termParser)
--- def structInstFieldAbbrev := leading_parser
---   -- `x` is an abbreviation for `x := x`
---   atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[" <|> (checkColGt "-" >> structInstFieldBinder)) "invalid field abbreviation")
 def optEllipsis := leading_parser
   optional " .."
 /-