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