Zulip Chat Archive

Stream: lean4

Topic: Is there a way to use equality of pattern in the case?


James Browning (Dec 24 2022 at 06:25):

Suppose I have:

match n with
| 0 => expr1
| m+1 => expr2

Is it possible to somehow capture the fact that m+1 = n and use it in expr2? (Specifically I want m < n, but this is trivial with the equality and )

Calvin Lee (Dec 24 2022 at 06:46):

Yes, if I recall the syntax correctly then

match h : n with
| 0 => expr1 -- h : n = 0
| m+1 => expr2 -- h : n = m + 1

James Browning (Dec 24 2022 at 06:53):

Awesome, exactly what I wanted thanks


Last updated: Dec 20 2023 at 11:08 UTC