feat: add Expr.getAppRevArgs

library/Init/Lean/Expr.lean

@@ -168,6 +168,13 @@ let dummy := Expr.sort Level.zero;
 let nargs := e.getAppNumArgs;
 getAppArgsAux e (mkArray nargs dummy) (nargs-1)
 
+private def getAppRevArgsAux : Expr → Array Expr → Array Expr
+| Expr.app f a, as => getAppRevArgsAux f (as.push a)
+| _,            as => as
+
+@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
+getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
+
 def isAppOf (e : Expr) (n : Name) : Bool :=
 match e.getAppFn with
 | Expr.const c _ => c == n

tests/lean/run/expr1.lean

@@ -0,0 +1,16 @@
+import Init.Lean.Expr
+open Lean
+
+def tst1 : IO Unit :=
+do let f   := Expr.const `f [];
+   let a   := Expr.const `a [];
+   let b   := Expr.const `b [];
+   let t   := mkApp f #[a, b, b];
+   let as₁ := t.getAppArgs;
+   let as₂ := t.getAppRevArgs;
+   IO.println as₁;
+   IO.println as₂;
+   unless (as₁.reverse == as₂) $ throw "failed";
+   pure ()
+
+#eval tst1