[Agda] optional dot in dot patterns?

Nils Anders Danielsson nad at chalmers.se
Mon Nov 19 11:57:18 CET 2012

On 2012-11-19 10:05, Peter Divianszky wrote:
> Function calls could be recognized by checking whether there is a
> function with that name in scope.

What about shadowing?

> In case of constructor calls (like .6) the expression and the pattern
> should be the same so maybe the compiler could figure out that 6 is a
> pattern match or a dot pattern. Is this true?

Sometimes it matters where you put the dots. Consider the following data

   data D : Set where
     d₁ d₂ : D

The following definition is OK:

   foo : (x y : D) → x ≡ y → D
   foo .d₁ d₁ refl = d₁
   foo _   d₂ _    = d₂

However, the following isn't (incomplete pattern matching):

   bar : (x y : D) → x ≡ y → D
   bar d₁ .d₁ refl = d₁
   bar _   d₂ _    = d₂

Let's add a final absurd clause:

   bar : (x y : D) → x ≡ y → D
   bar d₁ .d₁ refl = d₁
   bar _   d₂ _    = d₂
   bar d₂  d₁ ()

Now we have foo x d₂ eq = d₂ (definitionally, for variables x and eq),
but not bar x d₂ eq = d₂.


More information about the Agda mailing list