@@ -21,8 +21,6 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
21 (g1 : a -> b) -> (g2 : b -> c) ->
21 (g1 : a -> b) -> (g2 : b -> c) ->
22 map (g2 . g1) x = (map g2 . map g1) x
22 map (g2 . g1) x = (map g2 . map g1) x
24−-- TODO VerifiedFunctor instances for: List, Stream, Either e
26VerifiedFunctor Maybe where
24VerifiedFunctor Maybe where
27 functorIdentity Nothing = Refl
25 functorIdentity Nothing = Refl
28 functorIdentity (Just x) = Refl
26 functorIdentity (Just x) = Refl
@@ -57,8 +55,6 @@ VerifiedApplicative Maybe where
57 applicativeInterchange x Nothing = Refl
55 applicativeInterchange x Nothing = Refl
58 applicativeInterchange x (Just y) = Refl
56 applicativeInterchange x (Just y) = Refl
60−-- TODO VerifiedApplicative instances for: List, Stream, Either e
62interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
58interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
63 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
59 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
64 mf <*> mx = mf >>= \f =>
60 mf <*> mx = mf >>= \f =>
@@ -80,8 +76,6 @@ VerifiedMonad Maybe where
80 monadAssociativity Nothing f g = Refl
76 monadAssociativity Nothing f g = Refl
81 monadAssociativity (Just x) f g = Refl
77 monadAssociativity (Just x) f g = Refl
83−-- TODO VerifiedMonad instances for: List, Stream, Either e
85interface Semigroup a => VerifiedSemigroup a where
79interface Semigroup a => VerifiedSemigroup a where
86 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
80 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -100,16 +94,6 @@ implementation VerifiedSemigroup (List a) where
100[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
94[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
101 semigroupOpIsAssociative = multAssociativeZ
95 semigroupOpIsAssociative = multAssociativeZ
103−-- TODO Verified versions of...
104−-- (Semigroup m, Semigroup n) => Semigroup (m, n) where
105−-- (a, b) <+> (c, d) = (a <+> c, b <+> d)
107−-- Semigroup (Maybe a)
109−-- [collectJust] Semigroup a => Semigroup (Maybe a)
111−-- libs/base/Data/Morphisms.idr: implementation Monoid (Endomorphism a)
113interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
97interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
114 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
98 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
115 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
99 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
@@ -134,12 +118,6 @@ implementation VerifiedMonoid (List a) where
134 monoidNeutralIsNeutralL = appendNilRightNeutral
118 monoidNeutralIsNeutralL = appendNilRightNeutral
135 monoidNeutralIsNeutralR xs = Refl
119 monoidNeutralIsNeutralR xs = Refl
137−-- TODO Verified versions of...
138−-- (Monoid m, Monoid n) => Monoid (m, n) where
139−-- neutral = (neutral, neutral)
143interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
121interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
144 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
122 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
145 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
123 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral