[Agda] optional dot in dot patterns?

[Peter Divianszky]

On 19/11/2012 17:52, Dan Doel wrote:
>      data Vec (A : Set) : Nat -> Set where
>          nil : Vec A 0
>          cons : (n : Nat) -> A -> Vec A n -> Vec A (suc n)
>
>      foo : (A : Set) -> (n : Nat) -> Vec A n -> ...
>      foo A 0 nil = ...
>      foo A (suc n) (cons n x xs) = ...
>
> Which patterns are dotted in foo?

The second 'n' in the second alternative, because otherwise it would be 
repeated definition of 'n'.
Indeed this works, I tried

--------------------------------
foo : (A : Set) -> (n : Nat) -> Vec A n -> Vec A n
foo A 0 nil = nil
foo A (suc n) (cons .n x xs) = cons n x xs
--------------------------------

If you don't like the fact that 'foo' does pattern matching on the Nat 
argument, you could write

--------------------------------
foo : (A : Set) -> (n : Nat) -> Vec A n -> Vec A n
foo A .0 nil = nil
foo A .(suc n) (cons n x xs) = cons n x xs
--------------------------------

which would mean the same:

--------------------------------
foo : (A : Set) -> (n : Nat) -> Vec A n -> Vec A n
foo A .0 nil = nil
foo A .(suc n) (cons n x xs) = cons n x xs
--------------------------------





> On Mon, Nov 19, 2012 at 4:05 AM, Peter Divianszky <divipp at gmail.com> wrote:
>> Hi,
>>
>> Could the dot be optional in dot patterns?
>>
>> As I see there are three kinds of dot patterns:
>>
>> - function calls
>> - constructors calls
>> - variables
>>
>> Function calls could be recognized by checking whether there is a function
>> with that name in scope.
>> Variables could be recognized by checking whether there a variable with that
>> name in scope.
>> 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?
>>
>> Thanks,
>> Peter
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>