Zulip Chat Archive

Stream: new members

Topic: pattern matching in lambdas and props


view this post on Zulip Henning Dieterichs (Oct 23 2020 at 08:28):

Hey all! I'm new to Lean and was wondering whether
1) I can use pattern matching in lambdas (def fst := λ (x, y), x)
2) I can use pattern matching in props

lemma foo:  f: nat -> option nat, is_valid(f) ->  n: nat,
  match f(n) with
    | none := n = 1
    | (some val) := val = 2 * n
  end

However, it seems like I cannot use match there.

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:33):

Pattern matching in lambdas works for record types (aka structures), and may also others (I dunno)

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:33):

You can use match wherever you want

view this post on Zulip Reid Barton (Oct 23 2020 at 08:38):

1) needs to use the pointy brackets in the lambda, even if you're matching on prod specifically

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:39):

/me needs better glasses to distinguish those brackets on zulip

view this post on Zulip Reid Barton (Oct 23 2020 at 08:39):

2) works if you add a type, as indicated by the error message

view this post on Zulip Henning Dieterichs (Oct 23 2020 at 08:40):

Thanks, that fixed 2). I understood the error message as match not being supported in that context.

view this post on Zulip Henning Dieterichs (Oct 23 2020 at 08:41):

And \< \> solved 1). Thank you!


Last updated: May 11 2021 at 14:11 UTC