@@ -21,8 +21,6 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
2121 (g1 : a -> b) -> (g2 : b -> c) ->
2222 map (g2 . g1) x = (map g2 . map g1) x
2323
24−-- TODO VerifiedFunctor instances for: List, Stream, Either e
25−
2624VerifiedFunctor Maybe where
2725 functorIdentity Nothing = Refl
2826 functorIdentity (Just x) = Refl
@@ -57,8 +55,6 @@ VerifiedApplicative Maybe where
5755 applicativeInterchange x Nothing = Refl
5856 applicativeInterchange x (Just y) = Refl
5957
60−-- TODO VerifiedApplicative instances for: List, Stream, Either e
61−
6258interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
6359 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
6460 mf <*> mx = mf >>= \f =>
@@ -80,8 +76,6 @@ VerifiedMonad Maybe where
8076 monadAssociativity Nothing f g = Refl
8177 monadAssociativity (Just x) f g = Refl
8278
83−-- TODO VerifiedMonad instances for: List, Stream, Either e
84−
8579interface Semigroup a => VerifiedSemigroup a where
8680 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
8781
@@ -100,16 +94,6 @@ implementation VerifiedSemigroup (List a) where
10094[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
10195 semigroupOpIsAssociative = multAssociativeZ
10296
103−-- TODO Verified versions of...
104−-- (Semigroup m, Semigroup n) => Semigroup (m, n) where
105−-- (a, b) <+> (c, d) = (a <+> c, b <+> d)
106−--
107−-- Semigroup (Maybe a)
108−--
109−-- [collectJust] Semigroup a => Semigroup (Maybe a)
110−--
111−-- libs/base/Data/Morphisms.idr: implementation Monoid (Endomorphism a)
112−
11397interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
11498 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
11599 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
@@ -134,12 +118,6 @@ implementation VerifiedMonoid (List a) where
134118 monoidNeutralIsNeutralL = appendNilRightNeutral
135119 monoidNeutralIsNeutralR xs = Refl
136120
137−-- TODO Verified versions of...
138−-- (Monoid m, Monoid n) => Monoid (m, n) where
139−-- neutral = (neutral, neutral)
140−--
141−-- Monoid (Maybe a)
142−
143121interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
144122 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
145123 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral