or-patterns in match expressions

Stream: lean4

[Daniel Fabian]

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]

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]

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

[Leonardo de Moura]

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]

done. https://github.com/leanprover/lean4/issues/371