[Agda] question on `Any'
mechvel at botik.ru
Sun Aug 18 13:18:35 CEST 2013
On Tue, 2013-08-13 at 14:34 +0200, Dominique Devriese wrote:
> 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 _).
There are certain questions.
1) ``should be dotted'' or ``must be dotted'' ?
2) > the value of the underscore is fixed by the type of (here _)
But it is not fixed.
If x ≈ a, x ≈ b, then the value for the first underscore in the line
can be, say,
a :: , b :: a :: c :: , ...
The pattern .(_ :: _)
probably, tells ``some non-empty list over C'',
it looks sensible, and it is checked.
But what does this mean here `._'
-- this is a question.
The fact that it is type-checked looks strange.
More information about the Agda