From 0dc51ac7947ff6aa2c16bcffb64c46c7149d1276 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 Nov 2024 20:03:43 +1100 Subject: [PATCH] chore: fix two deprecations (#1061) --- Batteries/Lean/Expr.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Batteries/Lean/Expr.lean b/Batteries/Lean/Expr.lean index 98781ab0aa..17761cfaa0 100644 --- 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. -/