[Agda] Simple monoid instance based on monoid instance of underlying type

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Mon Jan 13 04:02:22 CET 2014


On 12/01/14 14:11, Andreas Abel wrote:
> There is a simple explanation for the error you see:
> 
>    There is no connection whatsover between the type \tau and the 
> carrier of the Monoid m.
> 
> To fix this, just use (Monoid.Carrier m) instead of \tau.  An voila, 
> suddenly things work like a charm! ;-)
> 
> [snip]

Ah, great, that's what I was looking for. Thanks!


-- 
Mateusz K.


More information about the Agda mailing list