[Agda] question on `Any'

[Dominique Devriese]

Sergei,

2013/8/13 Sergei Meshveliani <mechvel at botik.ru>:
> Please, why is not this type-checked
> (for  A : Setoid c l;  C = Carrier A)
> ?
>   open Any
>   f : (x : C) → (ys : List C) → Any (_≈_ x) ys → List C

Try changing the following line

>   f x _  (here _) = []

to use a dot pattern

  f x ._  (here _) = []

For more info, see the Agda tutorial by Norell and Chapman for
example.  They mention the following rule:
   The rule for when an argument should be dotted is: if there is a unique
   type correct value for the argument it should be dotted.

In this case, the value of the underscore is fixed by the type of (here _).

Regards,
Dominique