style of multiple `if let` expressions

Stream: mathlib4

[Floris van Doorn]

I want to use the following pattern:

if let some x := e1 then
  if let some y := e2 x then
    r1 x y
  else
    r2
else
  r2

However, r2 is a large term, so I don't want to write it twice. What is the preferred format to write this? The following is not great:

(if let some x := e1 then
  if let some y := e2 x then
    some <| r1 x y
  else
    none
else
  none).getD r2

Of course, it would be nice if we could write something like this:

if let some x := e1
   let some y := e2 x then
  r1 x y
else
  r2

[Kyle Miller]

You can do this at least:

def foo (e1 e2 : Option Nat) : Option Nat :=
  if let (some x, some y) := (e1, e2) then
    x + y
  else
    none

[Floris van Doorn]

Note that in my example e2 is applied to x.

[Sebastian Ullrich]

You can also do (heh)

Id.run do
  if let some x := e1 then
    if let some y := e2 x then
      return r1 x y
  r2

[Alex J. Best]

I think it would be great if lean 4 had lean 3 style multiple lets (in general but also in if let)
e.g. in lean 3 we could do

#eval let a := 1, b := 2 * a in b

but last I checked this wasn't possible in lean 4?

[Kyle Miller]

(@Sebastian Ullrich I was just writing that one! It seems like a reasonable construct to me, if a little surprising if you don't know the pattern.)

[Sebastian Ullrich]

If someone doesn't know the pattern, they should wonder about the highlighted return and hover over it!

[Sebastian Ullrich]

@Alex J. Best That's just let a := 1; let b := 2 * a; b, if let is a bit of a different beast

[Floris van Doorn]

That is a nice pattern @Sebastian Ullrich. I realize that the rest of the function I was editing would also be much nicer inside an Id.run do.

[Alex J. Best]

@Sebastian Ullrich sure the simple let version of my request is just a simple macro over let, but I believe it would make sense within if let too for situations like this: A comma separated list of assignments, where the if only succeeds if all the patterns can be matched giving access to the new variables in the match and nothing in the else statement.

[Marc Huisinga]

I think of Id.run as "go into imperative DSL mode". Some things are just nicer to express with control flow operators, loops and (locally) mutable variables.

[Sebastian Ullrich]

@Alex J. Best You might like https://github.com/leanprover/lean4/issues/1894, which proposes something even more general