## Stream: lean4

### Topic: or-patterns in match expressions

#### Daniel Fabian (Mar 27 2021 at 15:52):

Does lean 4 have or plan to have or-patterns like many ML languages?

def fib : Nat → Nat
| 0 | 1 => 1
| (n+2) => fib n + fib (n+1)


#### Leonardo de Moura (Mar 27 2021 at 16:16):

We don't have concrete plans to support it yet, but we can put it on the to-do list.
One very time-consuming part is specifying the new feature, and making sure it blends well with the existing ones.
Would you be interested in specifying this feature?

#### Daniel Fabian (Mar 27 2021 at 16:18):

sure, I'll take a stab at it and open a github issue with a proposed spec, how about that?

#### Leonardo de Moura (Mar 27 2021 at 17:33):

Daniel Fabian said:

sure, I'll take a stab at it and open a github issue with a proposed spec, how about that?

Thanks. A github issue is perfect.

#### Daniel Fabian (Mar 27 2021 at 18:32):

Last updated: May 07 2021 at 13:21 UTC