[Agda] Setoid for List

[Dr. ERDI Gergo]

On Wed, 9 Jan 2013, Joachim Breitner wrote:

> I also tried to give isEquiv, and it seems it worked, but agda still
> highlights eqRefl, eqSym and eqTrans in the last line as yellow, and I
> do not know why:
>
>    isEquiv : IsEquivalence eqList
>    isEquiv = record { refl = eqRefl ; sym = eqSym; trans = eqTrans }

That's just because implicit arguments don't seem to support this 
point-free style... If you change it to

     isEquiv : IsEquivalence eqList
     isEquiv = record { refl = λ {xs} → eqRefl {xs}
                      ; sym = λ {xs ys} → eqSym {xs} {ys}
                      ; trans = λ {xs ys zs} → eqTrans {xs} {ys} {zs}
                      }

then it should work.

Bye,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
<NyseriA> Things I've learned about war from videogames: If you find yourself mortally wounded by an enemy sniper be sure to let him know that he is a faggot.