Couple of small changes needed for Sept 2024

[brittAnderson]

I am running Lean (version 4.11.0-rc2, x86_64-unknown-linux-gnu, commit 0edf1bac392f, Release) and a few changes seem to have been made to the source and build hierarchy that leads to errors in your wc example. isEof no longer exists and the build subdir is now under lake.

I needed to change your IOfoldl definition to the following:

partial def IOfoldl {α} (f : α → UInt8 → α) (x : α) : IO α := do
  let stdin ← IO.getStdin
  let rdrslt ← stdin.read 4096
  if rdrslt.isEmpty
  then return x
  else 
    let x' := ByteArray.foldl f x rdrslt
    IOfoldl f x'

echo "The quick brown fox" | .lake/build/bin/wordcount

Your examples are some of the best brief intros. Hope we can keep them updated.