fix: incorrect antiquotation kind annotations

Apparently, none of them led to incorrect syntax trees, but `TSyntax`
still disapproves.

src/Lean/Elab/Deriving/BEq.lean

@@ -78,9 +78,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial then
-    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : Bool := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : Bool := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Deriving/DecEq.lean

@@ -88,7 +88,7 @@ def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
   let mut body   ← mkMatch header indVal auxFunName
   let binders    := header.binders
   let type       ← `(Decidable ($(mkIdent header.targetNames[0]) = $(mkIdent header.targetNames[1])))
-  `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : $type:term := $body:term)
+  `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term)
 
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
   let ctx ← mkContext "decEq" indVal.name

src/Lean/Elab/Deriving/FromToJson.lean

@@ -30,7 +30,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
           let (isOptField, nm) := mkJsonField field
           if isOptField then ``(opt $nm $(mkIdent <| header.targetNames[0] ++ field))
           else ``([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))])
-        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* :=
+        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:bracketedBinder* :=
           mkObj <| List.join [$fields,*])
         return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
       cmds.forM elabCommand
@@ -58,13 +58,14 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
             let xs ← xs.mapIdxM fun idx (x, t) => do
               `(($(quote userNames[idx].getString!), $(← mkToJson x t)))
             ``(mkObj [($(quote ctor.name.getString!), mkObj [$[$xs:term],*])])
-        let mut auxCmd ← `(match $[$discrs],* with $alts:matchAlt*)
-        if ctx.usePartial then
-          let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
-          auxCmd ← mkLet letDecls auxCmd
-          auxCmd ← `(private partial def $toJsonFuncId:ident $header.binders:explicitBinder* := $auxCmd)
-        else
-          auxCmd ← `(private def $toJsonFuncId:ident $header.binders:explicitBinder* := $auxCmd)
+        let auxTerm ← `(match $[$discrs],* with $alts:matchAlt*)
+        let auxCmd ←
+          if ctx.usePartial then
+            let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
+            let auxTerm ← mkLet letDecls auxTerm
+            `(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
+          else
+            `(private def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
         return #[auxCmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
       cmds.forM elabCommand
       return true
@@ -109,7 +110,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
         let jsonFields := fields.map (Prod.snd ∘ mkJsonField)
         let fields := fields.map mkIdent
-        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* (j : Json)
+        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:bracketedBinder* (j : Json)
           : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) := do
           $[let $fields:ident ← getObjValAs? j _ $jsonFields]*
           return { $[$fields:ident := $(id fields)],* })
@@ -123,22 +124,21 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let header ← mkHeader ``FromJson 0 ctx.typeInfos[0]
         let fromJsonFuncId := mkIdent ctx.auxFunNames[0]
         let alts ← mkAlts indVal fromJsonFuncId
-        let mut auxCmd ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
+        let mut auxTerm ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (← `(Except.error "no inductive constructor matched"))
         if ctx.usePartial then
           let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
-          auxCmd ← mkLet letDecls auxCmd
+          auxTerm ← mkLet letDecls auxTerm
         -- FromJson is not structurally recursive even non-nested recursive inductives,
         -- so we also use `partial` then.
-        if ctx.usePartial || indVal.isRec then
-          auxCmd ← `(
-            private partial def $fromJsonFuncId:ident $header.binders:explicitBinder* (json : Json)
-                : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) :=
-              $auxCmd)
-        else
-          auxCmd ← `(
-            private def $fromJsonFuncId:ident $header.binders:explicitBinder* (json : Json)
-                : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) :=
-              $auxCmd)
+        let auxCmd ←
+          if ctx.usePartial || indVal.isRec then
+            `(private partial def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
+                  : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) :=
+                $auxTerm)
+          else
+            `(private def $fromJsonFuncId:ident $header.binders:bracketedBinder* (json : Json)
+                  : Except String $(← mkInductiveApp ctx.typeInfos[0] header.argNames) :=
+                $auxTerm)
         return #[auxCmd] ++ (← mkInstanceCmds ctx ``FromJson declNames)
       cmds.forM elabCommand
       return true

src/Lean/Elab/Deriving/Hashable.lean

@@ -62,9 +62,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do
   let binders    := header.binders
   if ctx.usePartial then
     -- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
-    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : UInt64 := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : UInt64 := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : UInt64 := $body:term)
 
 def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Deriving/Inhabited.lean

@@ -77,8 +77,8 @@ where
       ctorArgs := ctorArgs.push (← `(_))
     for _ in [:ctorVal.numFields] do
       ctorArgs := ctorArgs.push (← ``(Inhabited.default))
-    let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs:ident*⟩)
-    `(instance $binders:explicitBinder* : $type := $val)
+    let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs*⟩)
+    `(instance $binders:bracketedBinder* : $type := $val)
 
   mkInstanceCmd? : TermElabM (Option Syntax) := do
     let ctorVal ← getConstInfoCtor ctorName

src/Lean/Elab/Deriving/Ord.lean

@@ -74,9 +74,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial || indVal.isRec then
-    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Ordering := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/Deriving/Repr.lean

@@ -94,9 +94,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial then
-    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : Format := $body:term)
+    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : Format := $body:term)
+    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Server/Rpc/Deriving.lean

@@ -143,7 +143,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
         $[($fieldIds : $fieldEncIds)]*
         deriving $(mkIdent ``FromJson), $(mkIdent ``ToJson)
 
-      instance : $(mkIdent ``RpcEncoding) $typeId $packetAppliedId:ident where
+      instance : $(mkIdent ``RpcEncoding) $typeId $packetAppliedId where
         rpcEncode a := return {
           $[$encInits],*
         }