fix DropWhile loop instance

2026-03-17 18:34:06 +00:00 · 2025-06-10 08:48:24 +02:00
1 changed files with 1 additions and 1 deletions
--- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
@@ -278,7 +278,7 @@ instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m
  .defaultImplementation

 instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoop α m n :=
+    IteratorLoop (DropWhile α m β P) m n :=
  .defaultImplementation

 instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]