[Agda] question on `Any'
dominique.devriese at cs.kuleuven.be
Tue Aug 13 14:34:25 CEST 2013
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 _).
More information about the Agda