mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 05:01:34 +03:00
d6370380e6
This was always the intended behaviour, but until now not implemented! This caught a couple of issues in contrib and a test.
23 lines
438 B
Idris
23 lines
438 B
Idris
module Control.Algebra.Implementations
|
|
|
|
import Control.Algebra
|
|
|
|
-- This file is for algebra implementations with nowhere else to go.
|
|
|
|
%default total
|
|
|
|
-- Functions ---------------------------
|
|
|
|
Semigroup (ty -> ty) where
|
|
(<+>) = (.)
|
|
|
|
SemigroupV (ty -> ty) where
|
|
semigroupOpIsAssociative _ _ _ = Refl
|
|
|
|
Monoid (ty -> ty) where
|
|
neutral = id
|
|
|
|
MonoidV (ty -> ty) where
|
|
monoidNeutralIsNeutralL _ = Refl
|
|
monoidNeutralIsNeutralR _ = Refl
|