## Stream: new members

### Topic: pattern matching in lambdas and props

#### 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.

#### Johan Commelin (Oct 23 2020 at 08:33):

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

#### Johan Commelin (Oct 23 2020 at 08:33):

You can use match wherever you want

#### 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

#### Johan Commelin (Oct 23 2020 at 08:39):

/me needs better glasses to distinguish those brackets on zulip

#### Reid Barton (Oct 23 2020 at 08:39):

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

#### 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.

#### Henning Dieterichs (Oct 23 2020 at 08:41):

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

Last updated: May 11 2021 at 14:11 UTC