fix: make getArg!' compute the correct arg index to access (#10567)

This PR fixes argument index calculation in `Lean.Expr.getArg!'`.

Author: sgraf812

src/Lean/Expr.lean

@@ -1267,7 +1267,7 @@ def getRevArg!' : Expr → Nat → Expr
   getRevArg! e (n - i - 1)
 
 /-- Similar to `getArg!`, but skips mdata -/
-@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
+@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs') : Expr :=
   getRevArg!' e (n - i - 1)
 
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/

tests/lean/run/getArgPrime.lean

@@ -0,0 +1,11 @@
+import Lean.Expr
+
+open Lean Expr
+
+example :
+  getArg! (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
+    = mkNatLit 2 := rfl
+
+example :
+  getArg!' (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
+    = mkNatLit 1 := rfl