how to return early

Stream: lean4

[Locria Cyber]

I've been wanting to do something like this

  let Option.some start := cavesys.indexOf? start
  | .none => []

[Jannis Limperg]

Can be done, and you even have almost the right syntax already:

-- only works in a do block
let (some start) := cavesys.indexOf? start
  | return ...

[Locria Cyber]

What's return used for?

[Locria Cyber]

Can I use it inside match? I only want to return early for some branches

[Jannis Limperg]

return a is equivalent to pure a except that it early-returns (and is therefore a keyword). So if you want an early return in a match, you just do

match x with
| c1 => return y
| c2 => return z
| c3 => ...

For the particular case where you want to early-return from all branches except one, you can use the syntax I showed:

let (c3) := x   -- note the parentheses; they are required
  | a
b

This is equivalent to

match x with
| c3 => b
| _ => a

In my example above, I used return in the early-return statement a, but you can put any monadic action there. In particular, I could have used pure as well since the early-returniness of return does not come into play there.

[Locria Cyber]

oh, I use .some instead

[Locria Cyber]

No parentheses needed

[Locria Cyber]

Without ., binding might not be constructor

[Locria Cyber]

let .some cavesys := CaveSystem.fromLines? lines

[Locria Cyber]

thanks for your info

[Jannis Limperg]

Ah, this must be a recent change; I'm pretty sure the parentheses were required at some point. Thanks!

[Locria Cyber]

    let fold :=
      match line.take 1 |> Substring.toString with
      | "x" => FoldAt.left ?hole
      | "y" => ?hol
      | other => return ()

[Locria Cyber]

seems like I can't use return here

[Sebastian Ullrich]

You need a corresponding do for early return

[Locria Cyber]

    let fold <-
      match line.take 1 |> Substring.toString with
      | "x" => pure $ .left foldAt
      | "y" => pure $ .up foldAt
      | _other =>
        IO.eprintln s!"Invalid instruction: {line} ; {_other}"
        return none

I solved it