max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: incorrect annotation

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-03 16:50:06 -07:00
parent a19e8fc526
commit b63eb886ce
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/BasicAux.lean
View file

@ -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 =>