diff --git a/libs/base/Data/Stream.idr b/libs/base/Data/Stream.idr index 792d99c0b..de903c436 100644 --- a/libs/base/Data/Stream.idr +++ b/libs/base/Data/Stream.idr @@ -124,6 +124,6 @@ Monad Stream where -- Properties -------------------------------------------------------------------------------- -lengthTake : (1 n : Nat) -> (xs : Stream a) -> length (take n xs) = n +lengthTake : (n : Nat) -> (xs : Stream a) -> length (take n xs) = n lengthTake Z _ = Refl lengthTake (S n) (x :: xs) = cong S (lengthTake n xs)