Andreas Reuleaux (7) [Avatar] Offline
"That is, in the pattern (x :: xs), word is a String, words is a vector of k Strings, and
for the output we need to provide a vector of Nat of length 1 + k, represented as S k."

should read (I would guess):
"That is, in the pattern (word :: words), ..."

(word::words) was introduced on p 74 already to make the pattern easier to read
Edwin Brady (65) [Avatar] Offline
Well spotted, thank you!