refactor: remove some unnecessary antiquotation kind annotations

2026-03-17 10:24:07 +00:00 · 2022-07-09 17:57:09 +02:00
parent cf380956a3
commit 5160cb7b0f
20 changed files with 74 additions and 76 deletions
--- a/doc/BoolExpr.lean
+++ b/doc/BoolExpr.lean
@@ -104,9 +104,9 @@ syntax entry := ident " ↦ " term:max
 syntax entry,* "⊢" term : term

 macro_rules
-  | `( $[$xs:ident ↦ $vs:term],* ⊢ $p:term ) =>
+  | `( $[$xs ↦ $vs],* ⊢ $p) =>
    let xs := xs.map fun x => quote x.getId.toString
-    `(denote (List.toAssocList [$[( $xs , $vs )],*]) `[BExpr| $p])
+    `(denote (List.toAssocList [$[($xs, $vs)],*]) `[BExpr| $p])

 #check b ↦ true ⊢ b ∨ b
 #eval  a ↦ false, b ↦ false ⊢ b ∨ a
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -176,10 +176,10 @@ The modifier `local` specifies the scope of the macro.
 /-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
    and then replaces `lhs` with `rhs`. -/
 local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
-  `((have h : $lhs:term = $rhs:term :=
+  `((have h : $lhs = $rhs :=
       -- TODO: replace with linarith
       by simp_arith at *; apply Nat.le_antisymm <;> assumption
-     try subst $lhs:term))
+     try subst $lhs))

 /-!
 The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
@@ -191,7 +191,7 @@ useful if `e` is the condition of an `if`-statement.
 -/
 /-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
 local macro "by_cases' " e:term :  tactic =>
-  `(by_cases $e:term <;> simp [*])
+  `(by_cases $e <;> simp [*])


 /-!
--- a/doc/metaprogramming-arith.lean
+++ b/doc/metaprogramming-arith.lean
@@ -18,9 +18,9 @@ syntax "`[Arith| " arith "]" : term
 macro_rules
  | `(`[Arith| $s:str]) => `(Arith.symbol $s)
  | `(`[Arith| $num:num]) => `(Arith.int $num)
-  | `(`[Arith| $x:arith + $y:arith]) => `(Arith.add `[Arith| $x] `[Arith| $y])
-  | `(`[Arith| $x:arith * $y:arith]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
-  | `(`[Arith| ($x:arith)]) => `(`[Arith| $x])
+  | `(`[Arith| $x + $y]) => `(Arith.add `[Arith| $x] `[Arith| $y])
+  | `(`[Arith| $x * $y]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
+  | `(`[Arith| ($x)]) => `(`[Arith| $x])

 #check `[Arith| "x" * "y"]  -- mul
 -- Arith.mul (Arith.symbol "x") (Arith.symbol "y")
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -129,14 +129,14 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
 syntax "by_cases" (atomic(ident ":"))? term : tactic

 macro_rules
-  | `(tactic| by_cases $h:ident : $e:term) =>
+  | `(tactic| by_cases $h : $e) =>
    `(tactic|
-      cases em $e:term with
-      | inl $h:ident => _
-      | inr $h:ident => _)
-  | `(tactic| by_cases $e:term) =>
+      cases em $e with
+      | inl $h => _
+      | inr $h => _)
+  | `(tactic| by_cases $e) =>
    `(tactic|
-      cases em $e:term with
+      cases em $e with
      | inl h => _
      | inr h => _)

--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -47,24 +47,22 @@ syntax (name := paren) "(" convSeq ")" : conv
 syntax (name := convConvSeq) "conv " " => " convSeq : conv

 /-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
-macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
-macro "rw " c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c:config]? $s:rwRuleSeq)
-macro "erw " s:rwRuleSeq : conv => `(rw (config := { transparency := Meta.TransparencyMode.default }) $s:rwRuleSeq)
+macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s) })
+macro "rw " c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c]? $s)
+macro "erw " s:rwRuleSeq : conv => `(rw (config := { transparency := Meta.TransparencyMode.default }) $s)

 macro "args" : conv => `(congr)
 macro "left" : conv => `(lhs)
 macro "right" : conv => `(rhs)
-syntax "intro " (colGt ident)* : conv
-macro_rules
-  | `(conv| intro $[$xs:ident]*) => `(conv| ext $xs*)
+macro "intro " xs:(colGt ident)* : conv => `(conv| ext $xs*)

 syntax enterArg := ident <|> ("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv
 macro_rules
  | `(conv| enter [$i:num]) => `(conv| arg $i)
-  | `(conv| enter [@$i:num]) => `(conv| arg @$i)
+  | `(conv| enter [@$i]) => `(conv| arg @$i)
  | `(conv| enter [$id:ident]) => `(conv| ext $id)
-  | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
+  | `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))

 macro "skip" : conv => `(tactic => rfl)
 macro "done" : conv => `(tactic' => done)
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1253,7 +1253,7 @@ end Meta
 namespace Parser.Tactic

 macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
-  `(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s:rwRuleSeq $[$loc:location]?)
+  `(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s $(loc)?)

 syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
 syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
@@ -1261,18 +1261,18 @@ syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
 macro "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
  let (kind, tkn, stx) ←
    if opt.raw.isNone then
-      pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
    else if opt.raw[0].getKind == ``simpAllKind then
-      pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
+      pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
    else
-      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
  `($stx:command
-    @[macro $tacName:ident] def expandSimp : Macro := fun s => do
+    @[macro $tacName] def expandSimp : Macro := fun s => do
      let c ← match s[1][0] with
-        | `(config| (config := $$c:term)) => `(config| (config := $updateCfg:term $$c))
-        | _ => `(config| (config := $updateCfg:term {}))
-      let s := s.setKind $kind:term
-      let s := s.setArg 0 (mkAtomFrom s[0] $tkn:term)
+        | `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
+        | _ => `(config| (config := $updateCfg {}))
+      let s := s.setKind $kind
+      let s := s.setArg 0 (mkAtomFrom s[0] $tkn)
      let r := s.setArg 1 (mkNullNode #[c])
      return r)

--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -29,7 +29,7 @@ def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type
      let ident := idents[i]![0]
      let acc ← match ident.isIdent, type? with
        | true,  none      => `($combinator fun $ident => $acc)
-        | true,  some type => `($combinator fun $ident:ident : $type => $acc)
+        | true,  some type => `($combinator fun $ident : $type => $acc)
        | false, none      => `($combinator fun _ => $acc)
        | false, some type => `($combinator fun _ : $type => $acc)
      loop i acc
@@ -67,12 +67,12 @@ syntax unifConstraintElem := colGe unifConstraint ", "?
 syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command

 macro_rules
-  | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
+  | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
    let mut body ← `($t₁ = $t₂)
    for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
      body ← `($c₁ = $c₂ → $body)
    let hint : Ident ← `(hint)
-    `($[$doc?:docComment]? @[$kind:attrKind unificationHint] def $(n.getD hint) $bs:bracketedBinder* : Sort _ := $body)
+    `($[$doc?:docComment]? @[$kind unificationHint] def $(n.getD hint) $bs* : Sort _ := $body)
 end Lean

 open Lean
@@ -224,13 +224,13 @@ syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
 macro_rules
  | `($mods:declModifiers class abbrev $id $params* $[: $ty]? := $[ $parents $[,]? ]*) =>
    let ctor := mkIdentFrom id <| id.raw[0].getId.modifyBase (. ++ `mk)
-    `($mods:declModifiers class $id $params* extends $[$parents:term],* $[: $ty]?
+    `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
      attribute [instance] $ctor)

 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax ("·" <|> ".") ppHardSpace many1Indent(tactic ";"? ppLine) : tactic
 macro_rules
-  | `(tactic| ·%$dot $[$tacs:tactic $[;%$sc]?]*) => `(tactic| {%$dot $[$tacs:tactic $[;%$sc]?]*})
+  | `(tactic| ·%$dot $[$tacs $[;%$sc]?]*) => `(tactic| {%$dot $[$tacs $[;%$sc]?]*})

 /--
  Similar to `first`, but succeeds only if one the given tactics solves the current goal.
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -205,7 +205,7 @@ syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic
 -/
 macro (name := rwSeq) rw:"rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
  match s with
-  | `(rwRuleSeq| [%$lbrak $rs:rwRule,* ]%$rbrak) =>
+  | `(rwRuleSeq| [%$lbrak $rs,* ]%$rbrak) =>
    -- We show the `rfl` state on `]`
    `(tactic| rewrite%$rw $(c)? [%$lbrak $rs,*] $(l)?; try (with_reducible rfl%$rbrak))
  | _ => Macro.throwUnsupported
@@ -280,7 +280,7 @@ macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
 /--
 `have h := e` adds the hypothesis `h : t` if `e : t`.
 -/
-macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x : _ := $p)
 /--
 Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`,
 `e` must have type `t` in the context `ctx, h : t'`.
@@ -288,7 +288,7 @@ Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal wi
 The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
 If `h :` is omitted, the name `this` is used.
 -/
-macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d:sufficesDecl; ?_)
+macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d; ?_)
 /--
 `let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`.
 If `t` is omitted, it will be inferred.
@@ -300,15 +300,15 @@ macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
 `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
 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
+macro "show " e:term : tactic => `(refine_lift show $e from ?_) -- TODO: fix, see comment
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
-  | `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
+  | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)

 -- Similar to `refineLift`, but using `refine'`
 macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right))
 macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
-macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
+macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : _ := $p)
 macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)

 syntax inductionAltLHS := "| " (("@"? ident) <|> "_") (ident <|> "_")*
@@ -397,7 +397,7 @@ macro_rules | `(tactic| trivial) => `(tactic| decide)
 macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
 macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)

-macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t:tacticSeq)
+macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t)

 /-- `fail msg` is a tactic that always fail and produces an error using the given message. -/
 syntax (name := fail) "fail " (str)? : tactic
--- a/src/Init/WFTactics.lean
+++ b/src/Init/WFTactics.lean
@@ -22,7 +22,7 @@ macro "decreasing_with " ts:tacticSeq : tactic =>
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
    first
-    | $ts:tacticSeq
+    | $ts
    | fail "failed to prove termination, possible solutions:\n  - Use `have`-expressions to prove the remaining goals\n  - Use `termination_by` to specify a different well-founded relation\n  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"))

 macro "decreasing_tactic" : tactic => `(decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial)
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -75,23 +75,23 @@ are turned into a new anonymous constructor application. For example,

@[builtinMacro Lean.Parser.Term.show] def expandShow : Macro := fun stx =>
  match stx with
-  | `(show $type from $val)            => let thisId := mkIdentFrom stx `this; `(let_fun $thisId : $type := $val; $thisId)
-  | `(show $type by%$b $tac:tacticSeq) => `(show $type from by%$b $tac:tacticSeq)
-  | _                                  => Macro.throwUnsupported
+  | `(show $type from $val)  => let thisId := mkIdentFrom stx `this; `(let_fun $thisId : $type := $val; $thisId)
+  | `(show $type by%$b $tac) => `(show $type from by%$b $tac)
+  | _                        => Macro.throwUnsupported

@[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
  let thisId := mkIdentFrom stx `this
  match stx with
  | `(have $x $bs* $[: $type]? := $val; $body)            => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have $[: $type]? := $val; $body)                    => `(have $thisId:ident $[: $type]? := $val; $body)
-  | `(have $x $bs* $[: $type]? $alts:matchAlts; $body)    => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
-  | `(have $[: $type]? $alts:matchAlts; $body)            => `(have $thisId:ident $[: $type]? $alts:matchAlts; $body)
+  | `(have $[: $type]? := $val; $body)                    => `(have $thisId $[: $type]? := $val; $body)
+  | `(have $x $bs* $[: $type]? $alts; $body)              => `(let_fun $x $bs* $[: $type]? $alts; $body)
+  | `(have $[: $type]? $alts:matchAlts; $body)            => `(have $thisId $[: $type]? $alts:matchAlts; $body)
  | `(have $pattern:term $[: $type]? := $val:term; $body) => `(let_fun $pattern:term $[: $type]? := $val:term ; $body)
-  | _                                                          => Macro.throwUnsupported
+  | _                                                     => Macro.throwUnsupported

@[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
  | `(suffices $[$x :]? $type from $val; $body)            => `(have $[$x]? : $type := $body; $val)
-  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have $[$x]? : $type := $body; by%$b $tac:tacticSeq)
+  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have $[$x]? : $type := $body; by%$b $tac)
  | _                                                           => Macro.throwUnsupported

 open Lean.Parser in
@@ -224,12 +224,12 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
  let some stx ← liftMacroM <| expandCDotArg? stx | pure none
  let stx ← liftMacroM <| expandMacros stx
  match stx with
-  | `(fun $binders* => $f:ident $args*) =>
+  | `(fun $binders* => $f $args*) =>
    if binders == args then
      try Term.resolveId? f catch _ => return none
    else
      return none
-  | `(fun $binders* => binop% $f:ident $a $b) =>
+  | `(fun $binders* => binop% $f $a $b) =>
    if binders == #[a, b] then
      try Term.resolveId? f catch _ => return none
    else
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -179,7 +179,7 @@ def elabDeclaration : CommandElab := fun stx => do
  match (← liftMacroM <| expandDeclNamespace? stx) with
  | some (ns, newStx) => do
    let ns := mkIdentFrom stx ns
-    let newStx ← `(namespace $ns:ident $(⟨newStx⟩) end $ns:ident)
+    let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns)
    withMacroExpansion stx newStx <| elabCommand newStx
  | none => do
    let decl     := stx[1]
@@ -259,7 +259,7 @@ def expandMutualNamespace : Macro := fun stx => do
  | some ns =>
    let ns := mkIdentFrom stx ns
    let stxNew := stx.setArg 1 (mkNullNode elemsNew)
-    `(namespace $ns:ident $(⟨stxNew⟩) end $ns:ident)
+    `(namespace $ns $(⟨stxNew⟩) end $ns)
  | none => Macro.throwUnsupported

@[builtinMacro Lean.Parser.Command.mutual]
--- a/src/Lean/Elab/MacroRules.lean
+++ b/src/Lean/Elab/MacroRules.lean
@@ -35,7 +35,7 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
      else
        throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
    | _ => throwUnsupportedSyntax
-  `($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)]
+  `($[$doc?:docComment]? @[$attrKind macro $(Lean.mkIdent k)]
    aux_def macroRules $(mkIdentFrom tk k) : Macro :=
     fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)

--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -927,7 +927,7 @@ where
            return mkHole ref
          else
            let id := mkIdentFrom ref localDecl.userName
-            `(?$id:ident)
+            `(?$id)
        else
          return mkHole ref
      let altViews  := altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
@@ -1148,7 +1148,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
              throwError "unexpected internal auxiliary discriminant name"
            let discrNew := discr.setArg 1 d
            let r ← loop discrs (discrsNew.push discrNew) foundFVars
-            `(let $d:ident := $term; $r)
+            `(let $d := $term; $r)
          match (← isAtomicDiscr? term) with
          | some x  => if x.isFVar then loop discrs (discrsNew.push discr) (foundFVars.insert x.fvarId!) else addAux
          | none    => addAux
@@ -1252,7 +1252,7 @@ matched on in dependent variables' types. Use `match (generalizing := true) ...`
 enforce this. -/
@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
  match stx with
-  | `(match $discr:term with | $y:ident => $rhs:term) =>
+  | `(match $discr:term with | $y:ident => $rhs) =>
     if (← isPatternVar y) then expandSimpleMatch stx discr y rhs expectedType? else elabMatchDefault stx expectedType?
  | _ => elabMatchDefault stx expectedType?
 where
@@ -1286,7 +1286,7 @@ e.g. because it has no constructors. -/
      elabMatchAux none #[discr] #[] mkNullNode expectedType
    | _ =>
      let d ← mkAuxDiscr
-      let stxNew ← `(let $d:ident := $discrExpr; nomatch $d:ident)
+      let stxNew ← `(let $d := $discrExpr; nomatch $d)
      withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
  | _ => throwUnsupportedSyntax

--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -94,7 +94,7 @@ def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Ma
  -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
  let lhs ← `($$f:ident)
  let lhs := Syntax.mkApp lhs (.mk args)
-  `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
+  `(@[$attrKind appUnexpander $(mkIdent c)]
    aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
      | `($lhs) => withRef f `($pat)
      | _       => throw ())
@@ -123,7 +123,7 @@ private def expandNotationAux (ref : Syntax)
     So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
  let fullName := currNamespace ++ name
  let pat : Term := ⟨mkNode fullName patArgs⟩
-  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat)
+  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio)) $[$syntaxParts]* : $cat)
  let macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
  let macroDecls ←
    if isLocalAttrKind attrKind then
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -251,7 +251,7 @@ partial def delab : Delab := do
  let stx ← delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
  if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then
    let typeStx ← withType delab
-    `(($stx:term : $typeStx:term)) >>= annotateCurPos
+    `(($stx : $typeStx)) >>= annotateCurPos
  else
    return stx

--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -233,7 +233,7 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
    let fieldPos ← nextExtraPos
    let fieldId := annotatePos fieldPos fieldId
    addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId fieldVals[idx]!
-    let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]):term)
+    let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]))
    fields := fields.push field
  let tyStx ← withType do
    if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
@@ -262,7 +262,7 @@ def delabAppImplicit : Delab := do
      let arg ← getExpr
      let opts ← getOptions
      let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
-        `(Parser.Term.namedArgument| ($(mkIdent name):ident := $argStx:term))
+        `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx))
      let argStx? : Option Syntax ←
        if ← getPPOption getPPAnalysisSkip then pure none
        else if ← getPPOption getPPAnalysisHole then `(_)
@@ -395,7 +395,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
        if let some hName := st.info.discrInfos[idx]!.hName? then
          -- TODO: we should check whether the corresponding binder name, matches `hName`.
          -- If it does not we should pretty print this `match` as a regular application.
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) }
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName) : $discr)) }
        else
          return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
      else if st.rhss.size < st.info.altNumParams.size then
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -256,12 +256,12 @@ where
        unless stx.isOfKind ``Lean.Parser.Command.declaration do
          return (syms, stxs')
        if let some stxRange := stx.getRange? then
-          let (name, selection) : String × Syntax := match stx with
-            | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $_) =>
+          let (name, selection) := match stx with
+            | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id$[.{$ls,*}]?]? $sig:declSig $_) =>
              ((·.getId.toString) <$> id |>.getD s!"instance {sig.raw.reprint.getD ""}", id.map (·.raw) |>.getD sig)
            | _ =>
              match stx.getArg 1 |>.getArg 1 with
-              | `(declId|$id:ident$[.{$ls,*}]?) => (id.raw.getId.toString, id)
+              | `(declId|$id$[.{$ls,*}]?) => (id.raw.getId.toString, id)
              | _ =>
                let stx10 : Syntax := (stx.getArg 1).getArg 0 -- TODO: stx[1][0] times out
                (stx10.isIdOrAtom?.getD "<unknown>", stx10)
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -20,9 +20,9 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
  -- TODO(WN): check that `typeNm` is not a scalar type
  let typeId := mkIdent typeNm
  let cmds ← `(
-    unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
+    unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef where
      rpcEncode := WithRpcRef.encodeUnsafe $(quote typeNm)
-      rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
+      rpcDecode := WithRpcRef.decodeUnsafeAs $typeId $(quote typeNm)

    @[implementedBy unsafeInst]
    opaque inst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef
@@ -97,7 +97,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr

    -- helpers for field initialization syntax
    let fieldInits (func : Name) := fieldIds.mapM fun fid =>
-      `(Parser.Term.structInstField| $fid:ident := ← $(mkIdent func):ident a.$fid:ident)
+      `(Parser.Term.structInstField| $fid:ident := ← $(mkIdent func) a.$fid)
    let encInits ← fieldInits ``rpcEncode
    let decInits ← fieldInits ``rpcDecode

--- a/tests/lean/run/liftMethodInMacrosIssue.lean
+++ b/tests/lean/run/liftMethodInMacrosIssue.lean
@@ -19,7 +19,7 @@ else
 syntax term "<|||>" term : doElem

 macro_rules
-| `(doElem| $a:term <|||> $b:term) => `(doElem| if (← $a:term) then pure true else $b:term)
+| `(doElem| $a:term <|||> $b) => `(doElem| if (← $a) then pure true else $b:term)

 def tst2 : IO Bool := do
 pure true <|||> (← throw $ IO.userError "failed")
--- a/tests/lean/run/obtain.lean
+++ b/tests/lean/run/obtain.lean
@@ -1,7 +1,7 @@


 macro "obtain " p:term " from " d:term "; " body:term : term =>
-`(match $d:term with | $p:term => $body:term)
+`(match $d:term with | $p => $body)

 theorem tst1 {p q r} (h : p ∧ q ∧ r) : q ∧ p ∧ r :=
 match h with
@@ -12,7 +12,7 @@ obtain ⟨h₁, ⟨h₂, h₃⟩⟩ from h;
 ⟨h₂, ⟨h₁, h₃⟩⟩

 macro "obtain " p:term " from " d:term : tactic =>
-`(tactic| match $d:term with | $p:term => ?hole)
+`(tactic| match $d:term with | $p => ?hole)

 theorem tst3 {p q r} (h : p ∧ q ∧ r) : q ∧ p ∧ r := by
  obtain ⟨h₁, ⟨h₂, h₃⟩⟩ from h