jreut (1) [Avatar] Offline
Listing 6.8 describes the implementation of `printf`. A `toFormat` helper is defined that recursively converts a `List Char` to a `Format`. The branch that handles literal strings follows:

toFormat : (xs : List Char) -> Format
toFormat (c :: chars) = case toFormat chars of
    Lit lit chars' => Lit (strCons c lit) chars'
    fmt => Lit (strCons c "") fmt

From what I can tell, the rationale behind pattern matching on `toFormat chars` is to fuse consecutive literal characters into one `Lit` type. Without some explanatory text, it took me a few minutes of exploration to figure it out. Of course, I love to figure things out on my own, but this particular confusion seems tangential to the purpose of this chapter.

I found changing some variable names in the expression helped me to understand the intention:

lit : String     -- maybe rename to `str` or `literalString`
chars' : Format  -- maybe rename to `fmt` or `format`

It's a fantastic read so far! Thanks to all involved in the language and this book!
Adam Gashlin (3) [Avatar] Offline
Agreed, when I typed this in I renamed chars' to fmt once I figured out what it was doing.