search

leanprover / fp-lean

Functional Programming in Lean
Other
70 stars 20 forks source link

Minor suggestion/observation for Ch 5 #161

Open TomasPuverle opened 1 month ago

TomasPuverle commented 1 month ago

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 commented 3 weeks ago

Absolutely, this is a great suggestion!