The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

441078 (1) [Avatar] Offline

In the chapter 3.2.3 ("Type, define, refine: sorting a vector"smilie, we begin with the listing 3.3 and we work through different iterations and interactions between code and repl.

The specific thing that doesn't work comes after the subtitle "Lifting Definitions" . There is a hole lifted to the toplevel. Then in this new definition we try to case-split the hole in then second case branch to insert a case construct:

insert : Ord elem => (x : elem) -> (xsSorted : Vect k elem) ->  Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = ?insert_rhs_2

insSort : Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                         insert x xsSorted

from the book: "Alternatively, you can use interactive editing to give more structure [...] . Press ctrl-Alt-M [...] over ?insert_rhs_2.

This doesn't work, for this code, I get the error:

When checking right hand side of insSort with expected type
Vect (S len) elem

Can't find implementation for Ord elem
Holes: Main.insSort, Main.insert_rhs_2