Questions tagged [pattern-matching]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

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 ...
tinlyx's user avatar
  • 1,772
4 votes
1 answer

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 ...
Nate Glenn's user avatar
1 vote
1 answer

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 ...
Agnishom Chattopadhyay's user avatar
3 votes
3 answers

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 ...
Celso Bonutti's user avatar
4 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: ...
Jeremy Salwen's user avatar
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 ...
ice1000's user avatar
  • 5,877