title: Agda: what does `.(` mean?
body: <p>I was looking at the code in <code>agda-stdlib/src/Data/Vec/Base.agda</code>
  and saw <code>.(</code> in</p>
  <pre><code>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
  </code></pre>
  <p>I tried removing the <code>.</code> in front of it and got the following error:</p>
  <pre><code>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
  </code></pre>
  <p>So I'm guessing it is necessary. But I don't understand what it is for exactly. I tried to look in <a href="https://agda.readthedocs.io/en/v2.6.1.1" rel="nofollow noreferrer">https://agda.readthedocs.io/en/v2.6.1.1</a> but couldn't find anything about it.</p>
  <p>Thanks!</p>