git.iko.soy/Idris-dev
on master help sign in
Minor cleanup
commit958d89e2b73a04de5317c7f6675d94719ae0e8b3 authorhowtonotwin <rasheeqhere@gmail.com> dateThu 29 Mar 2018, 13:20 (9 years ago) parenta6f9820
3 files changed+25−26
compare with master
unifiedsplit
libs/base/Data/Vect.idr+8−7 libs/contrib/Interfaces/Verified.idr+17−17 libs/prelude/Prelude/Algebra.idr−2
libs/base/Data/Vect.idr+8−7
@@ -571,12 +571,14 @@ range : {len : Nat} -> Vect len (Fin len)
571571range {len=Z} = []
572572range {len=S _} = FZ :: map FS range
573573
574−||| Transpose a Vect of Vects, turning rows into columns and vice versa.
574+||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
575+|||
576+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id`.
575577|||
576578||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
577−transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
578−transpose [] = replicate _ []
579−transpose (x :: xs) = zipWith (::) x (transpose xs)
579+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
580+transpose [] = replicate _ [] -- = [| [] |]
581+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
580582
581583--------------------------------------------------------------------------------
582584-- Applicative/Monad/Traversable
@@ -584,7 +586,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
584586
585587implementation Applicative (Vect k) where
586588 pure = replicate _
587−
588589 fs <*> vs = zipWith apply fs vs
589590
590591||| This monad is different from the List monad, (>>=)
@@ -593,8 +594,8 @@ implementation Monad (Vect len) where
593594 m >>= f = diag (map f m)
594595
595596implementation Traversable (Vect n) where
596− traverse f [] = pure Vect.Nil
597− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
597+ traverse f [] = pure []
598+ traverse f (x::xs) = [| f x :: traverse f xs |]
598599
599600--------------------------------------------------------------------------------
600601-- Show
libs/contrib/Interfaces/Verified.idr+17−17
@@ -100,7 +100,7 @@ VerifiedMonad Maybe where
100100 monadAssociativity (Just x) f g = Refl
101101
102102interface Semigroup a => VerifiedSemigroup a where
103− total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
103+ semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
104104
105105implementation VerifiedSemigroup (List a) where
106106 semigroupOpIsAssociative = appendAssociative
@@ -118,8 +118,8 @@ implementation VerifiedSemigroup (List a) where
118118 semigroupOpIsAssociative = multAssociativeZ
119119
120120interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
121− total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
122− total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
121+ monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
122+ monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
123123
124124[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
125125 monoidNeutralIsNeutralL = plusZeroRightNeutral
@@ -142,8 +142,8 @@ implementation VerifiedMonoid (List a) where
142142 monoidNeutralIsNeutralR xs = Refl
143143
144144interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
145− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
146− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
145+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
146+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
147147
148148VerifiedGroup ZZ using PlusZZMonoidV where
149149 groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
@@ -156,15 +156,15 @@ VerifiedGroup ZZ using PlusZZMonoidV where
156156 plusNegateInverseRZ k
157157
158158interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
159− total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
159+ abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
160160
161161VerifiedAbelianGroup ZZ where
162162 abelianGroupOpIsCommutative = plusCommutativeZ
163163
164164interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
165− total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
166− total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
167− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
165+ ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
166+ ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
167+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
168168
169169VerifiedRing ZZ where
170170 ringOpIsAssociative = multAssociativeZ
@@ -172,19 +172,19 @@ VerifiedRing ZZ where
172172 ringOpIsDistributiveR = multDistributesOverPlusLeftZ
173173
174174interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
175− total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
176− total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
175+ ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
176+ ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
177177
178178VerifiedRingWithUnity ZZ where
179179 ringWithUnityIsUnityL = multOneRightNeutralZ
180180 ringWithUnityIsUnityR = multOneLeftNeutralZ
181181
182182interface JoinSemilattice a => VerifiedJoinSemilattice a where
183− total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
184− total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
185− total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
183+ joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
184+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
185+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
186186
187187interface MeetSemilattice a => VerifiedMeetSemilattice a where
188− total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
189− total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
190− total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
188+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
189+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
190+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
libs/prelude/Prelude/Algebra.idr−2
@@ -18,7 +18,6 @@ infixl 6 <+>
1818interface Semigroup ty where
1919 (<+>) : ty -> ty -> ty
2020
21−
2221||| Sets equipped with a single binary operation that is associative, along with
2322||| a neutral element for that binary operation. Must satisfy the following
2423||| laws:
@@ -30,4 +29,3 @@ interface Semigroup ty where
3029||| forall a, neutral <+> a == a
3130interface Semigroup ty => Monoid ty where
3231 neutral : ty
33−