idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

Fix function name in one of the erasure examples #4911

Open hyphenrf opened 2 years ago

hyphenrf commented 2 years ago

Hi, first time contributing.. I found this while reading the docs.

The example still doesn't work without pattern matching on n too:

uninterleave : {n : Nat} -> Vect (n * 2) a -> (Vect n a, Vect n a)
uninterleave {n = Z} [] = ([] , [])
uninterleave {n = S n} (x :: y :: rest) with (uninterleave rest)
  | (xs, ys) = (x :: xs, y :: ys)