iv (2) [Avatar] Offline
#1
groupByN doesn't compile

When checking left hand side of with block in Main.groupByN:
    Can't match on with block in Main.groupByN a n (n_xs ++ rest) Exact


After fixing the code to:

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | Exact n_xs = n_xs :: groupByN n rest


I was able to proceed.

groupByN doesn't halt when n = 0

This can be seen in ex 2, where I effectively called groupByN (length [1] `div` 2) [1] = groupByN 0 [1]. Not sure if this is my fault, a bug in the exercise code or unclear instructions.
Edwin Brady (65) [Avatar] Offline
#2
I've fixed the error for the next version, thanks. I think I hadn't kept the text consistent with the code.

groupByN won't terminate if n is 0 (you'll see that Idris doesn't believe it's total, for this reason). I'll add a note on this, especially since termination is covered in the next section.
iv (2) [Avatar] Offline
#3
Thanks! It might also be good to be explicit about how halves should work when given an odd list. The [1] example kind of covers that, but I'd give an example with a longer list (e.g. [1..11]) and explicitly say why we choose to put the longer list second.