[Agda] optional dot in dot patterns?

[Dan Doel]

    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?

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