Questions tagged [pattern-matching]
The pattern-matching tag has no usage guidance.
6
questions
2
votes
1
answer
185
views
What is a pattern in dependent pattern matching?
I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
- 1,772
4
votes
1
answer
109
views
Why can addition be used in pattern matching Nats but not multiplication
Here's a simple dummy function in Lean 4:
def foo : Nat → Nat
| (m*2) => m
| (m+2) => m
| (m+1) => m
| (0) => 0
Lean has no trouble ...
- 197
1
vote
1
answer
125
views
How to deduce this equality based on the fact that these two terms must be the same?
Brief (but possibly inaccurate) Summary:
I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get ...
- 1,241
3
votes
3
answers
225
views
Pattern matching from `Prop` to `Type` in Lean
I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately.
I wanted to write a function like
...
4
votes
1
answer
690
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 247
4
votes
1
answer
76
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,877