From f7aebca12535aff8577e927e7f5bfc185c26e0c4 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 16 Aug 2024 19:04:06 -0400 Subject: [PATCH] fix: splitAtD reverse bug from #919 --- Batteries/Data/List/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 7e6e034dc4..679e8c505d 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -137,7 +137,7 @@ def splitAtD (n : Nat) (l : List α) (dflt : α) : List α × List α := go n l if `splitAtD n l dflt = (left, right)`. -/ go : Nat → List α → List α → List α × List α | n+1, x :: xs, acc => go n xs (x :: acc) - | 0, xs, acc => (acc, xs) + | 0, xs, acc => (acc.reverse, xs) | n, [], acc => (acc.reverseAux (replicate n dflt), []) /--