[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