# Tag Info

### 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,...
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 ...
• 9,104

### 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 ...
• 5,036
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 ...

### 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 ...
• 8,655
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 ...
• 9,104
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 ...
• 5,036
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 ...
• 8,655

### 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 ...
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 ...
• 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 ...

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