From 41c16951220aba787e37f36ebf920b5e1dffb4c5 Mon Sep 17 00:00:00 2001 From: Haz Date: Sat, 8 Jan 2022 14:45:14 +0200 Subject: [PATCH] Fix function name in one of the erasure examples Although the example still doesn't work without pattern matching on `n` too. --- docs/reference/erasure.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/reference/erasure.rst b/docs/reference/erasure.rst index 7f44c5a74f..2df36cea82 100644 --- a/docs/reference/erasure.rst +++ b/docs/reference/erasure.rst @@ -35,7 +35,7 @@ in the `original proposal uninterleave : {n : Nat} -> Vect (n * 2) a -> (Vect n a, Vect n a) uninterleave [] = ([] , []) - uninterleave (x :: y :: rest) with (unzipPairs rest) + uninterleave (x :: y :: rest) with (uninterleave rest) | (xs, ys) = (x :: xs, y :: ys) Notice that in this case, the second argument is the important one and