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