refactor: remove group(·)s

src/Init/Conv.lean

@@ -12,8 +12,8 @@ namespace Lean.Parser.Tactic.Conv
 
 declare_syntax_cat conv (behavior := both)
 
-syntax convSeq1Indented := withPosition((group(colGe conv ";"?))+)
-syntax convSeqBracketed := "{" (group(conv ";"?))+ "}"
+syntax convSeq1Indented := withPosition((colGe conv ";"?)+)
+syntax convSeqBracketed := "{" (conv ";"?)+ "}"
 -- Order is important: a missing `conv` proof should not be parsed as `{ <missing> }`,
 -- automatically closing goals
 syntax convSeq := convSeqBracketed <|> convSeq1Indented
@@ -58,7 +58,7 @@ syntax "intro " (colGt ident)* : conv
 macro_rules
   | `(conv| intro $[$xs:ident]*) => `(conv| ext $xs*)
 
-syntax enterArg := ident <|> group("@"? num)
+syntax enterArg := ident <|> ("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv
 macro_rules
   | `(conv| enter [$i:num]) => `(conv| arg $i)
@@ -72,7 +72,7 @@ macro "trace_state" : conv => `(tactic' => trace_state)
 macro "apply " e:term : conv => `(tactic => apply $e)
 
 /-- `first | conv | ...` runs each `conv` until one succeeds, or else fails. -/
-syntax (name := first) "first " withPosition((group(colGe "|" convSeq))+) : conv
+syntax (name := first) "first " withPosition((colGe "|" convSeq)+) : conv
 
 syntax "repeat " convSeq : conv
 macro_rules

src/Init/NotationExtra.lean

@@ -212,14 +212,14 @@ macro_rules
       attribute [instance] $ctor)
 
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
-syntax ("·" <|> ".") ppHardSpace many1Indent(group(tactic ";"? ppLine)) : tactic
+syntax ("·" <|> ".") ppHardSpace many1Indent(tactic ";"? ppLine) : tactic
 macro_rules
   | `(tactic| ·%$dot $[$tacs:tactic $[;%$sc]?]*) => `(tactic| {%$dot $[$tacs:tactic $[;%$sc]?]*})
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve " withPosition((group(colGe "|" tacticSeq))+) : tactic
+syntax (name := solve) "solve " withPosition((colGe "|" tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)

src/Init/Tactics.lean

@@ -141,7 +141,7 @@ syntax (name := withReducible) "with_reducible " tacticSeq : tactic
 syntax (name := withReducibleAndInstances) "with_reducible_and_instances " tacticSeq : tactic
 syntax (name := withUnfoldingAll) "with_unfolding_all " tacticSeq : tactic
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
-syntax (name := first) "first " withPosition((group(colGe "|" tacticSeq))+) : tactic
+syntax (name := first) "first " withPosition((colGe "|" tacticSeq)+) : tactic
 syntax (name := rotateLeft) "rotate_left" (num)? : tactic
 syntax (name := rotateRight) "rotate_right" (num)? : tactic
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
@@ -302,7 +302,7 @@ macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
  performs the unification, and replaces the target with the unified version of `t`.
 -/
 macro "show " e:term : tactic => `(refine_lift show $e:term from ?_) -- TODO: fix, see comment
-syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
+syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
   | `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
 
@@ -312,7 +312,7 @@ macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
 macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
 
-syntax inductionAltLHS := "| " (group("@"? ident) <|> "_") (ident <|> "_")*
+syntax inductionAltLHS := "| " (("@"? ident) <|> "_") (ident <|> "_")*
 syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
 /--