pattern matching in lambdas and props

Stream: new members

[Henning Dieterichs]

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]

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

[Johan Commelin]

You can use match wherever you want

[Reid Barton]

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

[Johan Commelin]

/me needs better glasses to distinguish those brackets on zulip

[Reid Barton]

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

[Henning Dieterichs]

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

[Henning Dieterichs]

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