git.iko.soy/Idris-dev
on master help sign in
Instance docs: add some instance docs to libs
9d45713Adam Sandberg Eriksson
libs/base/Data/VectType.idr+5−4
compare with master
unifiedsplit
@@ -1,4 +1,4 @@
1−module Data.VectType
1+module Data.VectType
2
2
3import Data.Fin
3import Data.Fin
4
4
@@ -6,7 +6,7 @@ import Data.Fin
6%default total
6%default total
7
7
8namespace Vect {
8namespace Vect {
9−
9+
10infixr 7 ::
10infixr 7 ::
11
11
12%elim data Vect : Nat -> Type -> Type where
12%elim data Vect : Nat -> Type -> Type where
@@ -531,6 +531,8 @@ instance Applicative (Vect k) where
531
531
532 fs <*> vs = zipWith apply fs vs
532 fs <*> vs = zipWith apply fs vs
533
533
534+||| This monad is different from the List monad, (>>=)
535+||| uses the diagonal.
534instance Monad (Vect n) where
536instance Monad (Vect n) where
535 m >>= f = diag (map f m)
537 m >>= f = diag (map f m)
536
538
@@ -539,7 +541,7 @@ instance Traversable (Vect n) where
539 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
541 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
540
542
541--------------------------------------------------------------------------------
543--------------------------------------------------------------------------------
542−-- Show
544+-- Show
543--------------------------------------------------------------------------------
545--------------------------------------------------------------------------------
544
546
545instance Show a => Show (Vect n a) where
547instance Show a => Show (Vect n a) where
@@ -595,4 +597,3 @@ instance DecEq a => DecEq (Vect n a) where
595
597
596-- For the primitives, we have to cheat because we don't have access to their
598-- For the primitives, we have to cheat because we don't have access to their
597-- internal implementations.
599-- internal implementations.
598−
libs/prelude/Prelude/Nat.idr+3−1
@@ -195,6 +195,7 @@ instance Num Nat where
195instance MinBound Nat where
195instance MinBound Nat where
196 minBound = Z
196 minBound = Z
197
197
198+||| Casts negative `Integers` to 0.
198instance Cast Integer Nat where
199instance Cast Integer Nat where
199 cast = fromInteger
200 cast = fromInteger
200
201
@@ -250,6 +251,7 @@ instance BoundedJoinSemilattice Nat where
250 bottom = Z
251 bottom = Z
251
252
252
253
254+||| Casts negative `Ints` to 0.
253instance Cast Int Nat where
255instance Cast Int Nat where
254 cast i = fromInteger (cast i)
256 cast i = fromInteger (cast i)
255
257
@@ -333,7 +335,7 @@ lcm x y = divNat (x * y) (gcd x y)
333
335
334
336
335--------------------------------------------------------------------------------
337--------------------------------------------------------------------------------
336−-- An informative comparison view
338+-- An informative comparison view
337--------------------------------------------------------------------------------
339--------------------------------------------------------------------------------
338data CmpNat : Nat -> Nat -> Type where
340data CmpNat : Nat -> Nat -> Type where
339 CmpLT : (y : _) -> CmpNat x (x + S y)
341 CmpLT : (y : _) -> CmpNat x (x + S y)