Skip to main content
7 votes

Binding variables to terms involving later variables

Great question Mike! Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently,...
James McKinna's user avatar
5 votes
Accepted

How to recover implicit arguments of inductive types in a match expression?

In Lean @foo is like foo but with all arguments made explicit, see documentation on implicit arguments (search for ...
Andrej Bauer's user avatar
  • 9,104
5 votes

Binding variables to terms involving later variables

Coq (and probably Lean too): The answer for (vanilla) Coq is simple: it does not. Nothing is done to n to remember its relation to the pattern in the branch. The ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

What is a pattern in dependent pattern matching?

So there's a few things going on here. The picture you show is actually 3 different tables, placed side by side to preserve space. This is a sad effect of page limits for papers. The first column is ...
Joey Eremondi's user avatar
5 votes

Why can addition be used in pattern matching Nats but not multiplication

The short answer is two fold: For a pattern to be matchable it has to be only using variables and the basic constructors for a given inductive/structure type. For ...
Jason Rute's user avatar
  • 8,655
5 votes
Accepted

Pattern matching from `Prop` to `Type` in Lean

There are situations in which every morphism $A \to B$ is constant: In topological spaces, if $A$ is a space with the trivial topology and $B$ is a $T_0$-space then a continuous map $A \to B$ is ...
Andrej Bauer's user avatar
  • 9,104
4 votes
Accepted

Is it a good idea to modify the context during type checking of patterns?

I would say that having a pattern-matching construct that works differently depending on whether its scrutinee is a variable or a more complex expression sounds like a very ad-hoc thing to do. It ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

Doing case-by-case proofs about match statements in Lean4

Note, this my not be the most optimal answer, but here is how I would approach this. Also, note, it is important to provide a MWE when you ask questions like this so that the answerer can plug this ...
Jason Rute's user avatar
  • 8,655
2 votes

How to deduce this equality based on the fact that these two terms must be the same?

This is a dependent inversion problem that has been bothering many Coq users. There is a short answer on Stack Overflow [1]. For your example, we have H before ...
Qinshi Wang's user avatar
1 vote

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

Dotted patterns are also known as inaccessible patterns. My understanding is that the matched bindings are inaccessible, because they are generated from index unification. That's why they are marked ...
ice1000's user avatar
  • 6,176
1 vote

Pattern matching from `Prop` to `Type` in Lean

Short answer (probably the same as on Zulip, I didn't check): With proof irrelevance it doesn't make sense to match on an inductive Prop. This is what this error ...
François G. Dorais's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible