git.iko.soy/Idris-dev
on master help sign in
Minor cleanup
958d89ehowtonotwin
libs/base/Data/Vect.idr+8−7
compare with master
unifiedsplit
@@ -571,12 +571,14 @@ range : {len : Nat} -> Vect len (Fin len)
571range {len=Z} = []
571range {len=Z} = []
572range {len=S _} = FZ :: map FS range
572range {len=S _} = FZ :: map FS range
573
573
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`.
575|||
577|||
576||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
578||| 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)
579+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
578−transpose [] = replicate _ []
580+transpose [] = replicate _ [] -- = [| [] |]
579−transpose (x :: xs) = zipWith (::) x (transpose xs)
581+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
580
582
581--------------------------------------------------------------------------------
583--------------------------------------------------------------------------------
582-- Applicative/Monad/Traversable
584-- Applicative/Monad/Traversable
@@ -584,7 +586,6 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
584
586
585implementation Applicative (Vect k) where
587implementation Applicative (Vect k) where
586 pure = replicate _
588 pure = replicate _
587−
588 fs <*> vs = zipWith apply fs vs
589 fs <*> vs = zipWith apply fs vs
589
590
590||| This monad is different from the List monad, (>>=)
591||| This monad is different from the List monad, (>>=)
@@ -593,8 +594,8 @@ implementation Monad (Vect len) where
593 m >>= f = diag (map f m)
594 m >>= f = diag (map f m)
594
595
595implementation Traversable (Vect n) where
596implementation Traversable (Vect n) where
596− traverse f [] = pure Vect.Nil
597+ traverse f [] = pure []
597− traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
598+ traverse f (x::xs) = [| f x :: traverse f xs |]
598
599
599--------------------------------------------------------------------------------
600--------------------------------------------------------------------------------
600-- Show
601-- Show
libs/contrib/Interfaces/Verified.idr+17−17
@@ -100,7 +100,7 @@ VerifiedMonad Maybe where
100 monadAssociativity (Just x) f g = Refl
100 monadAssociativity (Just x) f g = Refl
101
101
102interface Semigroup a => VerifiedSemigroup a where
102interface 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
104
104
105implementation VerifiedSemigroup (List a) where
105implementation VerifiedSemigroup (List a) where
106 semigroupOpIsAssociative = appendAssociative
106 semigroupOpIsAssociative = appendAssociative
@@ -118,8 +118,8 @@ implementation VerifiedSemigroup (List a) where
118 semigroupOpIsAssociative = multAssociativeZ
118 semigroupOpIsAssociative = multAssociativeZ
119
119
120interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
120interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
121− total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
121+ monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
122− total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
122+ monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
123
123
124[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
124[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
125 monoidNeutralIsNeutralL = plusZeroRightNeutral
125 monoidNeutralIsNeutralL = plusZeroRightNeutral
@@ -142,8 +142,8 @@ implementation VerifiedMonoid (List a) where
142 monoidNeutralIsNeutralR xs = Refl
142 monoidNeutralIsNeutralR xs = Refl
143
143
144interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
144interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
145− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
145+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
146− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
146+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
147
147
148VerifiedGroup ZZ using PlusZZMonoidV where
148VerifiedGroup ZZ using PlusZZMonoidV where
149 groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
149 groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
@@ -156,15 +156,15 @@ VerifiedGroup ZZ using PlusZZMonoidV where
156 plusNegateInverseRZ k
156 plusNegateInverseRZ k
157
157
158interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
158interface (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
160
160
161VerifiedAbelianGroup ZZ where
161VerifiedAbelianGroup ZZ where
162 abelianGroupOpIsCommutative = plusCommutativeZ
162 abelianGroupOpIsCommutative = plusCommutativeZ
163
163
164interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
164interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
165− total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
165+ 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)
166+ 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)
167+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
168
168
169VerifiedRing ZZ where
169VerifiedRing ZZ where
170 ringOpIsAssociative = multAssociativeZ
170 ringOpIsAssociative = multAssociativeZ
@@ -172,19 +172,19 @@ VerifiedRing ZZ where
172 ringOpIsDistributiveR = multDistributesOverPlusLeftZ
172 ringOpIsDistributiveR = multDistributesOverPlusLeftZ
173
173
174interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
174interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
175− total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
175+ ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
176− total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
176+ ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
177
177
178VerifiedRingWithUnity ZZ where
178VerifiedRingWithUnity ZZ where
179 ringWithUnityIsUnityL = multOneRightNeutralZ
179 ringWithUnityIsUnityL = multOneRightNeutralZ
180 ringWithUnityIsUnityR = multOneLeftNeutralZ
180 ringWithUnityIsUnityR = multOneLeftNeutralZ
181
181
182interface JoinSemilattice a => VerifiedJoinSemilattice a where
182interface JoinSemilattice a => VerifiedJoinSemilattice a where
183− total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
183+ 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
184+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
185− total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
185+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
186
186
187interface MeetSemilattice a => VerifiedMeetSemilattice a where
187interface MeetSemilattice a => VerifiedMeetSemilattice a where
188− total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
188+ 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
189+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
190− total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
190+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
libs/prelude/Prelude/Algebra.idr−2
@@ -18,7 +18,6 @@ infixl 6 <+>
18interface Semigroup ty where
18interface Semigroup ty where
19 (<+>) : ty -> ty -> ty
19 (<+>) : ty -> ty -> ty
20
20
21−
22||| Sets equipped with a single binary operation that is associative, along with
21||| Sets equipped with a single binary operation that is associative, along with
23||| a neutral element for that binary operation. Must satisfy the following
22||| a neutral element for that binary operation. Must satisfy the following
24||| laws:
23||| laws:
@@ -30,4 +29,3 @@ interface Semigroup ty where
30||| forall a, neutral <+> a == a
29||| forall a, neutral <+> a == a
31interface Semigroup ty => Monoid ty where
30interface Semigroup ty => Monoid ty where
32 neutral : ty
31 neutral : ty
33−