Pattern match actions

Stream: lean4

[J. O.]

How do i pattern match on actions, since the manual says that it is TODO

[Mario Carneiro]

You are going to have to give more context. What do you mean by "actions"?

[Mario Carneiro]

do you have a #mwe with an example of what you want to write?

[Chris B]

The do notation section of the manual introduces "action" as a term of art. They define it as function application when the return type is m a for some monad m.

[Mario Carneiro]

I suspected that might be the meaning, but it would be weird to pattern match on actions in most cases

[Mario Carneiro]

is this talking about lean 3's do some x <- m | return false, ...?

[Chris B]

I think the meaning is this deal:

match (<- thing) with
| _ => ...

when thing is of type m α.

[Chris B]

Oh yeah there's that too.

[Mario Carneiro]

For the version you just wrote I don't see what extra sugar is needed

[Mario Carneiro]

lean 4 does have if let some x <- m then ... else return false already, so I guess this is just about the let-else pattern

[Chris B]

You should put those in the manual :eyes:

[Chris B]

I gave it a shot. https://github.com/leanprover/lean4/pull/990

[Marc Huisinga]

Mario Carneiro said:

is this talking about lean 3's do some x <- m | return false, ...?

This works in Lean 4 too:

def bar : Option Nat := some 0

def foo : Bool := Id.run do
  let some x ← bar | return false
  return x = 0