git.iko.soy/Idris-dev
on master help sign in
whitespaces
ecb2818raichoo
idris.cabal+2−2
compare with master
unifiedsplit
@@ -14,7 +14,7 @@ Description: Idris is a general purpose language with full dependent types.
14 Dependent types allow types to be predicated on values,
14 Dependent types allow types to be predicated on values,
15 meaning that some aspects of a program's behaviour can be
15 meaning that some aspects of a program's behaviour can be
16 specified precisely in the type. The language is closely
16 specified precisely in the type. The language is closely
17− related to Epigram and Agda. There is a tutorial at
17+ related to Epigram and Agda. There is a tutorial at
18 <http://www.idris-lang.org/documentation>.
18 <http://www.idris-lang.org/documentation>.
19 Features include:
19 Features include:
20 .
20 .
@@ -459,7 +459,7 @@ Library
459 if os(freebsd)
459 if os(freebsd)
460 cpp-options: -DFREEBSD
460 cpp-options: -DFREEBSD
461 build-depends: unix
461 build-depends: unix
462− if os(dragonfly)
462+ if os(dragonfly)
463 cpp-options: -DDRAGONFLY
463 cpp-options: -DDRAGONFLY
464 build-depends: unix
464 build-depends: unix
465 if os(darwin)
465 if os(darwin)
libs/prelude/Prelude.idr+3−3
@@ -334,7 +334,7 @@ instance Traversable (Vect n) where
334 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
334 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
335
335
336---- some mathematical operations
336---- some mathematical operations
337−---- XXX this should probably go some place else,
337+---- XXX this should probably go some place else,
338pow : (Num a) => a -> Nat -> a
338pow : (Num a) => a -> Nat -> a
339pow x Z = 1
339pow x Z = 1
340pow x (S n) = x * (pow x n)
340pow x (S n) = x * (pow x n)
@@ -376,7 +376,7 @@ instance Enum Integer where
376 enumFromThen n inc = n :: enumFromThen (inc + n) inc
376 enumFromThen n inc = n :: enumFromThen (inc + n) inc
377 enumFromTo n m = if n <= m
377 enumFromTo n m = if n <= m
378 then go (natRange (S (cast {to = Nat} (m - n))))
378 then go (natRange (S (cast {to = Nat} (m - n))))
379− else []
379+ else []
380 where go : List Nat -> List Integer
380 where go : List Nat -> List Integer
381 go [] = []
381 go [] = []
382 go (x :: xs) = n + cast x :: go xs
382 go (x :: xs) = n + cast x :: go xs
@@ -392,7 +392,7 @@ instance Enum Int where
392 toNat n = cast n
392 toNat n = cast n
393 fromNat n = cast n
393 fromNat n = cast n
394 enumFromThen n inc = n :: enumFromThen (inc + n) inc
394 enumFromThen n inc = n :: enumFromThen (inc + n) inc
395− enumFromTo n m = if n <= m
395+ enumFromTo n m = if n <= m
396 then go (natRange (S (cast {to = Nat} (m - n))))
396 then go (natRange (S (cast {to = Nat} (m - n))))
397 else []
397 else []
398 where go : List Nat -> List Int
398 where go : List Nat -> List Int