Difference between inaccessible term and wildcard

Stream: new members

[Joao Bregunci]

I was reading the Lean Reference Manual to understand a little bit more about the equation compiler and in the chapter 4.7 it states that a pattern matching definition can be one of the following:

---

• a variable, denoting an arbitrary value of the relevant type
• an underscore, denoting a wildcard or anonymous variable,
• an inaccessible term
• a constructor for the inductive type of the corresponding argument, applied to a sequence of patterns

---

The first, second and the fourth definitions above I can distinguish easily, but I am having a hard time understanding the value of an inaccessible term. In the reference manual it states that inaccessible terms are the following:

---

"An expression of the form .(t) in a pattern is known as an inaccessible term. It is not viewed as part of
the pattern; rather, it is explicit information that is used by the elaborator and equation compiler when
interpreting the definition. Inaccessible terms do not participate in pattern matching. They are sometimes
needed for a pattern to make sense, for example, when a constructor depends on a parameter that is not
a pattern-matching variable. In other cases, they can be used to inform the equation compiler that certain
arguments do not require a case split, and they can be used to make a definition more readable."

---

To me it seems strange that I simply don't put an _ in all entries of the variable that is not useful for the pattern match, instead of _.. Also it seems strange to me that it states the it does not participate in pattern matching, but follows with the following code:

variable {α : Type u}
def add [has_add α] :
Π {n : N}, vector α n → vector α n → vector α n
| ._ nil nil := nil
| ._ (cons a v) (cons b w) := cons (a + b) (add v w)

def add' [has_add α] :
Π {n : N}, vector α n → vector α n → vector α n
| .(0) nil nil := nil
| .(n+1) (@cons .(α) n a v) (cons b w) := cons (a + b) (add' v w)

The number of elements of the vector in the second example in above code is not used for a pattern match? I feel that I don't understand very well when I should use this inacessible term in my pattern match.

[Mario Carneiro]

Note that a late addition to lean 3 automatically infers when a _ should be a ._, and as a result inaccessible terms are essentially never needed anymore

[Mario Carneiro]

the only reason you would use it is in an example like add' where for documentation reasons you want to say that the first case has a 0 for n and the second has n+1. Lean already knows this so you can just write _, but if you want to write 0 then it has to be .(0) so that it isn't interpreted as a pattern match on n