@@ -85,37 +85,35 @@ record Multiplicative : Set where
8585record Additive : Set where
8686 getAdditive : Nat -> Additive
8787
88−instance Semigroup Multiplicative where
89− left <.> right = getMultiplicative $ left' * right'
90− where
91− left' : Nat
92− left' =
93− case left of
94− getMultiplicative m => m
95−
96− right' : Nat
97− right' =
98− case right of
99− getMultiplicative m => m
100−
101−instance Semigroup Additive where
102− left <.> right = getAdditive $ left' + right'
103− where
104− left' : Nat
105− left' =
106− case left of
107− getAdditive m => m
108−
109− right' : Nat
110− right' =
111− case right of
112− getAdditive m => m
113−
114−instance Monoid Multiplicative where
115− neutral = getMultiplicative $ S O
116−
117−instance Monoid Additive where
118− neutral = getAdditive $ O
88+-- XXX: infix operators don't seem to be being exported correctly from
89+-- algebra.idr?
90+--instance Monoid Multiplicative where
91+-- neutral = getMultiplicative $ S O
92+-- left <+> right = getMultiplicative $ left' * right'
93+-- where
94+-- left' : Nat
95+-- left' =
96+-- case left of
97+-- getMultiplicative m => m
98+
99+-- right' : Nat
100+-- right' =
101+-- case right of
102+-- getMultiplicative m => m
103+
104+--instance Monoid Additive where
105+-- neutral = getAdditive $ O
106+-- left <+> right = getAdditive $ left' + right'
107+-- where
108+-- left' : Nat
109+-- left' =
110+-- case left of
111+-- getAdditive m => m
112+
113+-- right' : Nat
114+-- right' =
115+-- case right of
116+-- getAdditive m => m
119117
120118--------------------------------------------------------------------------------
121119-- Auxilliary notions