Let pattern matching

Stream: lean4

[Daniel Weber]

Currently pattern matching with let doesn't keep the definition of the value. I believe this conflicts with the rest of the behavior of let and is confusing (example 1, example 2, example 3), and so should either:

1. be removed/linted against, and have pattern := value will have to be used instead.
2. be changed so it keeps the definition - e.g. let (a, b) := l will behave like let a := l.1; let b := l.2 - this would probably require quite some effort, I'm not sure how pattern matching is implemented.

[Eric Wieser]

If you want to "keep the value", you can use match h : value with pattern => instead

[Eric Wieser]

But 1) sounds quite reasonable to me

[Daniel Weber]

Should I make an RFC?

[Daniel Weber]

lean4#5216