Understanding a basic error.

Stream: new members

[Will King]

I was working through this example of programming in Lean 4 https://lean-lang.org/functional_programming_in_lean/hello-world/cat.html

I got to this function

def fileStream (filename: System.FilePath) : IO (Option IO.FS.Stream) := do
  if not filename.pathExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle IO.FS.handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

I get an error unexpected token '('; expected ')' based on that last line. The highlighted error in VS code suggests it is the second opening parenthesis (some _(_ that is causing the issue.

The questions I have are:

• What is going on and how can I address this issue?
• Where can I find resources to diagnose issues such as this? My initial search on duckduckgo wasn't very helpful so I'd love any resources people can point me to.

[Patrick Massot]

I think the previous line looks fishy.

[Kyle Miller]

It looks like your let is missing an ← or :=

[Kyle Miller]

According to the original fileStream in the book, it's missing an arrow after handle

[Will King]

Thanks so much. That was the problem.