diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 9d247413c1..6bd09bcb56 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -458,9 +458,9 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
           | _ => undecided
         doMatch := fun yes no => do
           let prefixDiscrs ← (List.range idx).mapM (`(Syntax.getArg __discr $(quote ·)))
-          let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (__discr.getNumArgs - $(quote numSuffix))))
+          let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (Nat.sub __discr.getNumArgs $(quote numSuffix))))
           let suffixDiscrs ← (List.range numSuffix).mapM fun i =>
-            `(Syntax.getArg __discr (__discr.getNumArgs - $(quote (numSuffix - i))))
+            `(Syntax.getArg __discr (Nat.sub __discr.getNumArgs $(quote (numSuffix - i))))
           `(ite (GE.ge __discr.getNumArgs $(quote (quoted.getNumArgs - 1)))
               $(← yes (prefixDiscrs ++ sliceDiscr :: suffixDiscrs))
               $(← no))
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index 47a56d1b96..485c27df30 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -62,7 +62,7 @@
               let_fun __discr_4 := Lean.Syntax.getArg __discr_3 1;
               let_fun __discr_5 :=
                 Lean.mkNullNode
-                  (Array.extract (Lean.Syntax.getArgs __discr_3) 2 (Lean.Syntax.getNumArgs __discr_3 - 0));
+                  (Array.extract (Lean.Syntax.getArgs __discr_3) 2 (Nat.sub (Lean.Syntax.getNumArgs __discr_3) 0));
               let_fun moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs __discr_5);
               let_fun rhs := { raw := __discr_4 };
               let_fun lhs := { raw := __discr };