Minor suggestion/observation for Ch 5

[TomasPuverle]

Reading the first section of Ch 5 with the andThen code, I see e.g.

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? fun first =>
  andThen xs[2]? fun third =>
  some (first, third)

Given that I just finished Ch 4 (esp. 4.6 on coercions) where it says "This allows option types to be used in a manner even more similar to nullable types, because some can be omitted", I am wondering why I have to/should say some in the code above. Would you consider adding a note on this? Thanks!

[david-christiansen]

Absolutely, this is a great suggestion!