on master help sign in
whitespaces
commitecb2818773ea5ff0dd41f8374a628767e9e10f75 authorraichoo <raichoo@googlemail.com> dateFri 17 Jan 2014, 17:38 (13 years ago) parentf24ae1d
2 files changed+5−5
idris.cabal+2−2 libs/prelude/Prelude.idr+3−3
idris.cabal+2−2
@@ -14,7 +14,7 @@ Description: Idris is a general purpose language with full dependent types.
1414 Dependent types allow types to be predicated on values,
1515 meaning that some aspects of a program's behaviour can be
1616 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
1818 <http://www.idris-lang.org/documentation>.
1919 Features include:
2020 .
@@ -459,7 +459,7 @@ Library
459459 if os(freebsd)
460460 cpp-options: -DFREEBSD
461461 build-depends: unix
462− if os(dragonfly)
462+ if os(dragonfly)
463463 cpp-options: -DDRAGONFLY
464464 build-depends: unix
465465 if os(darwin)
libs/prelude/Prelude.idr+3−3
@@ -334,7 +334,7 @@ instance Traversable (Vect n) where
334334 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
335335
336336---- some mathematical operations
337−---- XXX this should probably go some place else,
337+---- XXX this should probably go some place else,
338338pow : (Num a) => a -> Nat -> a
339339pow x Z = 1
340340pow x (S n) = x * (pow x n)
@@ -376,7 +376,7 @@ instance Enum Integer where
376376 enumFromThen n inc = n :: enumFromThen (inc + n) inc
377377 enumFromTo n m = if n <= m
378378 then go (natRange (S (cast {to = Nat} (m - n))))
379− else []
379+ else []
380380 where go : List Nat -> List Integer
381381 go [] = []
382382 go (x :: xs) = n + cast x :: go xs
@@ -392,7 +392,7 @@ instance Enum Int where
392392 toNat n = cast n
393393 fromNat n = cast n
394394 enumFromThen n inc = n :: enumFromThen (inc + n) inc
395− enumFromTo n m = if n <= m
395+ enumFromTo n m = if n <= m
396396 then go (natRange (S (cast {to = Nat} (m - n))))
397397 else []
398398 where go : List Nat -> List Int