Zulip Chat Archive

Stream: new members

Topic: Understanding a basic error.

Will King (Dec 12 2023 at 22:36):

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
    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 (Dec 12 2023 at 22:41):

I think the previous line looks fishy.

Kyle Miller (Dec 12 2023 at 22:41):

It looks like your let is missing an or :=

Kyle Miller (Dec 12 2023 at 22:46):

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

Will King (Dec 12 2023 at 23:00):

Thanks so much. That was the problem.

Last updated: Dec 20 2023 at 11:08 UTC