Questions tagged [pattern-matching]
The pattern-matching tag has no usage guidance.
2
questions
2
votes
1
answer
89
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 217
4
votes
1
answer
75
views
Is it a good idea to modify the context during type checking of patterns?
So I'm working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have ...
- 5,424