From c3585dbbbbd35d08f8a9bbe4a793dfd6dfc2f2ec Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 24 Jun 2022 14:10:04 +0200
Subject: [PATCH] chore: raw syntax kind accesses

Sometimes just checking the kind simply is the simplest solution.
---
 src/Lean/Elab/BuiltinNotation.lean               | 2 +-
 src/Lean/Elab/Quotation.lean                     | 4 ++--
 src/Lean/Elab/Syntax.lean                        | 2 +-
 src/Lean/Elab/Term.lean                          | 2 +-
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 4 ++--
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 89957b68c7..9c5ff46b96 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -108,7 +108,7 @@ private def elabParserMacroAux (prec e : TSyntax `term) (withAnonymousAntiquot :
 @[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab :=
   adaptExpander fun stx => match stx with
   | `(leading_parser $[: $prec?]? $[(withAnonymousAntiquot := $anon?)]? $e) =>
-    elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.isOfKind ``Parser.Term.trueVal))
+    elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.raw.isOfKind ``Parser.Term.trueVal))
   | _ => throwUnsupportedSyntax
 
 private def elabTParserMacroAux (prec lhsPrec e : TSyntax `term) : TermElabM Syntax := do
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index ceacf26219..ccfcc39eaf 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -545,8 +545,8 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
   match stx with
   | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     if !patss.any (·.any (fun
-      | `($_@$pat) => pat.isQuot
-      | pat         => pat.isQuot)) then
+      | `($_@$pat) => pat.raw.isQuot
+      | pat        => pat.raw.isQuot)) then
       -- no quotations => fall back to regular `match`
       throwUnsupportedSyntax
     let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 5a70ae522a..273a904e1e 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -343,7 +343,7 @@ def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
 
 def inferMacroRulesAltKind : TSyntax ``matchAlt → CommandElabM SyntaxNodeKind
   | `(matchAltExpr| | $pat:term => $_) => do
-    if !pat.isQuot then
+    if !pat.raw.isQuot then
       throwUnsupportedSyntax
     let quoted := getQuotContent pat
     pure quoted.getKind
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index b0ccbce943..81d7bd0b7e 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1102,7 +1102,7 @@ private def isExplicitApp (stx : Syntax) : Bool :=
   Example: `fun {α} (a : α) => a` -/
 private def isLambdaWithImplicit (stx : Syntax) : Bool :=
   match stx with
-  | `(fun $binders* => $_) => binders.any fun b => b.isOfKind ``Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
+  | `(fun $binders* => $_) => binders.raw.any fun b => b.isOfKind ``Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
   | _                      => false
 
 private partial def dropTermParens : Syntax → Syntax := fun stx =>
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 33633bdc1a..d81a74fc1c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -166,7 +166,7 @@ def delabAppExplicit : Delab := do
   let (fnStx, _, argStxs) ← withAppFnArgs
     (do
       let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabAppFn
-      let needsExplicit := stx.getKind != ``Lean.Parser.Term.explicit
+      let needsExplicit := stx.raw.getKind != ``Lean.Parser.Term.explicit
       let stx ← if needsExplicit then `(@$stx) else pure stx
       pure (stx, paramKinds.toList, #[]))
     (fun ⟨fnStx, paramKinds, argStxs⟩ => do
@@ -705,7 +705,7 @@ def delabNamedPattern : Delab := do
   let p ← withAppFn $ withAppArg delab
   -- TODO: we should hide `h` if it has an inaccessible name and is not used in the rhs
   let h ← withAppArg delab
-  guard x.isIdent
+  guard x.raw.isIdent
   `($x:ident@$h:ident:$p:term)
 
 -- Sigma and PSigma delaborators