From b63eb886ceedcdac102b0a1f3e5fe7d61839cf49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Nov 2022 16:50:06 -0700 Subject: [PATCH] chore: incorrect annotation --- src/Init/Data/List/BasicAux.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index d573de18fb..1d895b8c64 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -184,7 +184,7 @@ theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where antisymm h₁ h₂ := le_antisymm h₁ h₂ -@[inline] private unsafe def mapMonoMImp [Monad m] (as : List α) (f : α → m α) : m (List α) := do +@[specialize] private unsafe def mapMonoMImp [Monad m] (as : List α) (f : α → m α) : m (List α) := do match as with | [] => return as | b :: bs =>