Zulip Chat Archive

Stream: lean4

Topic: or-patterns in match expressions


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Mar 27 2021 at 18:32):

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


Last updated: May 07 2021 at 13:21 UTC