feat: stx[i] as notation for stx.getArg i

src/Init/LeanInit.lean

@@ -248,6 +248,10 @@ match stx with
 | Syntax.node _ args => args.get! i
 | _                  => Syntax.missing -- panic! "Syntax.getArg: not a node"
 
+-- Add `stx[i]` as sugar for `stx.getArg i`
+@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax :=
+self.getArg idx
+
 def getArgs (stx : Syntax) : Array Syntax :=
 match stx with
 | Syntax.node _ args => args

src/Lean/Elab/Tactic/Basic.lean

@@ -249,22 +249,22 @@ modifyMCtx fun mctx => do
   pure mctx
 
 @[builtinTactic seq1] def evalSeq1 : Tactic :=
-fun stx => (stx.getArg 0).forSepArgsM evalTactic
+fun stx => stx[0].forSepArgsM evalTactic
 
 @[builtinTactic paren] def evalParen : Tactic :=
-fun stx => evalSeq1 (stx.getArg 1)
+fun stx => evalSeq1 stx[1]
 
 @[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
-fun stx => stx.getArg 0 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
+fun stx => stx[0].forArgsM fun seqElem => evalTactic seqElem[0]
 
 @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
-fun stx => withRef (stx.getArg 2) $ focus $ stx.getArg 1 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
+fun stx => withRef stx[2] $ focus $ stx[1].forArgsM fun seqElem => evalTactic seqElem[0]
 
 @[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
-fun stx => focus $ evalTactic (stx.getArg 1)
+fun stx => focus $ evalTactic stx[1]
 
 @[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
-fun stx => evalTactic (stx.getArg 0)
+fun stx => evalTactic stx[0]
 
 partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
 | i =>
@@ -284,7 +284,7 @@ fun stx => pure ()
 
 @[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic :=
 fun stx => do
-  let tactic := stx.getArg 1
+  let tactic := stx[1]
   if (← do try evalTactic tactic; pure true catch _ => pure false) then
     throwError "tactic succeeded"
 
@@ -318,7 +318,7 @@ fun stx => match_syntax stx with
 
 @[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic :=
 fun stx => do
-  let matchAlts := stx.getArg 1
+  let matchAlts := stx[1]
   let stxNew ← liftMacroM $ Term.expandMatchAltsIntoMatchTactic stx matchAlts
   withMacroExpansion stx stxNew $ evalTactic stxNew
 

src/Lean/Elab/Tactic/Binders.lean

@@ -24,7 +24,7 @@ fun stx => do
 
 @[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro :=
 fun stx =>
-  let type := stx.getArg 1
+  let type := stx[1]
   `(tactic| refine (show $type from ?_))
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Generalize.lean

@@ -13,11 +13,11 @@ namespace Lean.Elab.Tactic
 open Meta
 
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if (stx.getArg 1).isNone then none
-else some ((stx.getArg 1).getIdAt 0)
+if stx[1].isNone then none
+else some stx[1][0].getId
 
 private def getVarName (stx : Syntax) : Name :=
-stx.getIdAt 4
+stx[4].getId
 
 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
 let tag    ← Meta.getMVarTag mvarId
@@ -68,7 +68,7 @@ match h? with
 fun stx => do
   let h? := getAuxHypothesisName stx
   let x  := getVarName stx
-  let e ← elabTerm (stx.getArg 2) none
+  let e ← elabTerm stx[2] none
   evalGeneralizeAux h? e x
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Induction.lean

@@ -17,13 +17,13 @@ open Meta
 -- Recall that
 -- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if stx.getArg 1 $.getArg 0 $.isNone then
+if stx[1][0].isNone then
   none
 else
-  some $ stx.getArg 1 $.getArg 0 $.getIdAt 0
+  some stx[1][0][0].getId
 
 private def getMajor (stx : Syntax) : Syntax :=
-stx.getArg 1 $.getArg 1
+stx[1][1]
 
 private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
 match h? with
@@ -57,12 +57,12 @@ match major with
   `stx` is syntax for `induction`. -/
 private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
 withRef stx $
-let generalizingStx := stx.getArg 3
+let generalizingStx := stx[3]
 if generalizingStx.isNone then
   pure #[]
 else withMainMVarContext do
   trace `Elab.induction fun _ => generalizingStx
-  let vars := (generalizingStx.getArg 1).getArgs
+  let vars := generalizingStx[1].getArgs
   getFVarIds vars
 
 -- process `generalizingVars` subterm of induction Syntax `stx`.
@@ -75,16 +75,16 @@ liftMetaTacticAux fun mvarId => do
   pure (fvarIds.size, [mvarId'])
 
 private def getAlts (withAlts : Syntax) : Array Syntax :=
-withAlts.getArg 2 $.getSepArgs
+withAlts[2].getSepArgs
 
 /-
   Given an `inductionAlt` of the form
   ```
   nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
   ``` -/
-private def getAltName (alt : Syntax) : Name := (alt.getArg 0).getId.eraseMacroScopes
-private def getAltVarNames (alt : Syntax) : Array Name := (alt.getArg 1).getArgs.map Syntax.getId
-private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
+private def getAltName (alt : Syntax) : Name := alt[0].getId.eraseMacroScopes
+private def getAltVarNames (alt : Syntax) : Array Name := alt[1].getArgs.map Syntax.getId
+private def getAltRHS (alt : Syntax) : Syntax := alt[3]
 
 /-
   Given alts of the form
@@ -98,7 +98,7 @@ for alt in alts do
   let n := getAltName alt
   withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
   unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
-    throwErrorAt! (alt.getArg 0) "invalid constructor name '{n}'"
+    throwErrorAt! alt[0] "invalid constructor name '{n}'"
 
 structure RecInfo :=
 (recName : Name)
@@ -199,8 +199,8 @@ else
   ``` -/
 private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo :=
 withRef stx do
-let usingRecStx := stx.getArg 2
-let withAlts    := stx.getArg 4
+let usingRecStx := stx[2]
+let withAlts    := stx[4]
 if usingRecStx.isNone then
   let (rinfo, _) ← getRecInfoDefault major withAlts false
   pure rinfo
@@ -317,7 +317,7 @@ fun stx => focusAux do
   let major ← elabMajor h? (getMajor stx)
   let major ← generalizeMajor major
   let (mvarId, _) ← getMainGoal
-  let withAlts := stx.getArg 2
+  let withAlts := stx[2]
   let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true
   let result ← Meta.cases mvarId major.fvarId! recInfo.altVars
   checkCasesResult result ctorNames recInfo.altRHSs

src/Lean/Elab/Tactic/Injection.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic
 -- optional (" with " >> many1 ident')
 private def getInjectionNewIds (stx : Syntax) : List Name :=
 if stx.isNone then []
-else stx.getArg 1 $.getArgs.toList.map Syntax.getId
+else stx[1].getArgs.toList.map Syntax.getId
 
 private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := do
 unless unusedIds.isEmpty do
@@ -20,8 +20,8 @@ unless unusedIds.isEmpty do
 @[builtinTactic «injection»] def evalInjection : Tactic :=
 fun stx => do
   -- parser! nonReservedSymbol "injection " >> termParser >> withIds
-  let fvarId ← elabAsFVar (stx.getArg 1)
-  let ids := getInjectionNewIds (stx.getArg 2)
+  let fvarId ← elabAsFVar stx[1]
+  let ids := getInjectionNewIds stx[2]
   liftMetaTactic fun mvarId => do
     match ← Meta.injection mvarId fvarId ids (!ids.isEmpty) with
     | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; pure []

src/Lean/Elab/Tactic/Location.lean

@@ -21,13 +21,13 @@ def location         := parser! "at " >> (locationWildcard <|> locationTarget <|
 ```
 -/
 def expandLocation (stx : Syntax) : Location :=
-let arg := stx.getArg 1
+let arg := stx[1]
 if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
 else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
-else Location.localDecls $ arg.getArg 0 $.getArgs.map fun stx => stx.getId
+else Location.localDecls $ arg[0].getArgs.map fun stx => stx.getId
 
 def expandOptLocation (stx : Syntax) : Location :=
 if stx.isNone then Location.target
-else expandLocation $ stx.getArg 0
+else expandLocation stx[0]
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Match.lean

@@ -15,11 +15,11 @@ structure AuxMatchTermState :=
 (cases   : Array Syntax := #[])
 
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
-let matchAlts := matchTac.getArg 4
-let alts      := matchAlts.getArg 1 $.getArgs
+let matchAlts := matchTac[4]
+let alts      := matchAlts[1].getArgs
 let newAlts ← alts.mapSepElemsM fun alt => do
   let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
-  let holeOrTacticSeq := alt.getArg 2
+  let holeOrTacticSeq := alt[2]
   if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
     pure alt
   else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
@@ -30,7 +30,7 @@ let newAlts ← alts.mapSepElemsM fun alt => do
     pure $ alt.setArg 2 newHole
   else withFreshMacroScope do
     let newHole ← `(?rhs)
-    let newHoleId := newHole.getArg 1
+    let newHoleId := newHole[1]
     let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
     modify fun s => { s with cases := s.cases.push newCase }
     pure $ alt.setArg 2 newHole

src/Lean/Elab/Tactic/Rewrite.lean

@@ -14,8 +14,8 @@ open Meta
 
 @[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro :=
 fun stx =>
-  let seq := ((stx.getArg 1).getArg 1).getSepArgs
-  let loc := stx.getArg 2
+  let seq := stx[1][1].getSepArgs
+  let loc := stx[2]
   pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[mkAtomFrom rwRule "rewrite ", rwRule, loc]
 
 def rewriteTarget (stx : Syntax) (symm : Bool) : TacticM Unit := do
@@ -59,10 +59,10 @@ def «rewrite» := parser! "rewrite" >> rwRule >> optional location
 -/
 @[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic :=
 fun stx => do
-  let rule := stx.getArg 1
-  let symm := !(rule.getArg 0).isNone
-  let term := rule.getArg 1
-  let loc  := expandOptLocation $ stx.getArg 2
+  let rule := stx[1]
+  let symm := !rule[0].isNone
+  let term := rule[1]
+  let loc  := expandOptLocation stx[2]
   match loc with
   | Location.target => rewriteTarget term symm
   | Location.localDecls userNames => userNames.forM (rewriteLocalDecl term symm)