I was looking at the code in agda-stdlib/src/Data/Vec/Base.agda
and saw .(
in
take : ∀ m {n} → Vec A (m + n) → Vec A m
take m xs with splitAt m xs
take m .(ys ++ zs) | (ys , zs , refl) = ys
I tried removing the .
in front of it and got the following error:
Could not parse the left-hand side
take m (ys ++ zs) | (ys , zs , refl)
Operators used in the grammar:
++ (infixr operator, level 5) [_++_ (/Users/fss/Dropbox/Documents/projects/Coding/dev/agda/agda-stdlib/src/Data/Vec/Base.agda:99,1-5)]
, (infixr operator, level 4) [_,_ (/usr/local/Cellar/agda/2.6.1/share/x86_64-osx-ghc-8.10.1/Agda-2.6.1/lib/prim/Agda/Builtin/Sigma.agda:9,15-18)]
when scope checking the left-hand side
take m (ys ++ zs) | (ys , zs , refl) in the definition of take
So I'm guessing it is necessary. But I don't understand what it is for exactly. I tried to look in https://agda.readthedocs.io/en/v2.6.1.1 but couldn't find anything about it.
Thanks!
First off, in
the pattern
ys ++ zs
is not valid because it is not a constructor applied on other patterns. If you think about it, in general it doesn't make sense to pattern match as function application because you'd need to be able to invert every function.However, in
we pattern match on the result of
splitAt
as well. The type of the third argument is(ys ++ zs) == xs
, and the type of the constructorrefl
is(ys ++ zs) == (ys ++ zs)
. By unification, that meansxs ~ (ys ++ zs)
, so the second argument totake
cannot be anything other thanys ++ zs
in this clause.And this is exactly what a dot-pattern means: