[Agda] strange mismatch

[Sergei Meshveliani]

On Fri, 2017-05-26 at 01:03 -0500, Andrés Sicard-Ramírez wrote:
> On 25 May 2017 at 11:40, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > For example, for the equation
> >
> >     f (con zr) _ = con zr
> >
> > in the above context we have that
> > zr  in the pattern is a variable to be matched,
> > and  zr  on the right-hand side is the one in the parameters.
> > Right?
> 
> No. The `zr` on the RHS is also the variable in the pattern.
> 

And where this zr will be taken from the parameters?
I expect that in this clause:

    f _ _ = con zr
?

------
Sergei