Questions tagged [pattern-matching]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

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

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