chore: deprecate Expr.lambdaArity in favor of existing upstream ver…

…sion (#992)

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Batteries/Lean/Expr.lean

@@ -24,6 +24,9 @@ def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
   mvar.mvarId!.assign e
   pure stx
 
+@[deprecated (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
+abbrev lambdaArity := @getNumHeadLambdas
+
 /--
 Returns the number of leading `∀` binders of an expression. Ignores metadata.
 -/
@@ -32,13 +35,9 @@ def forallArity : Expr → Nat
   | forallE _ _ body _ => 1 + forallArity body
   | _ => 0
 
-/--
-Returns the number of leading `λ` binders of an expression. Ignores metadata.
--/
-def lambdaArity : Expr → Nat
-  | mdata _ b => lambdaArity b
-  | lam _ _ b _ => 1 + lambdaArity b
-  | _ => 0
+-- TODO: replace `forallArity` after https://github.com/leanprover/lean4/pull/5729
+-- @[deprecated (since := "2024-10-16"), inherit_doc getNumHeadForalls]
+-- abbrev forallArity := @getNumHeadForalls
 
 /-- Like `getAppNumArgs` but ignores metadata. -/
 def getAppNumArgs' (e : Expr) : Nat :=