chore: fix two deprecations (#1061)

leanprover-community · Nov 23, 2024 · 0dc51ac · 0dc51ac
1 parent 8b52587
commit 0dc51ac
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Batteries/Lean/Expr.lean b/Batteries/Lean/Expr.lean
@@ -24,10 +24,10 @@ def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
   mvar.mvarId!.assign e
   pure stx
 
-@[deprecated (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
+@[deprecated getNumHeadLambdas (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
 abbrev lambdaArity := @getNumHeadLambdas
 
-@[deprecated (since := "2024-11-13"), inherit_doc getNumHeadForalls]
+@[deprecated getNumHeadForalls(since := "2024-11-13"), inherit_doc getNumHeadForalls]
 abbrev forallArity := @getNumHeadForalls
 
 /-- Like `withApp` but ignores metadata. -/