git.iko.soy/Idris-dev
on master help sign in
Make it compile, and use a List instead of a Vect

- It was necessary to add the new file lib/Prelude/Bits.idr to lib/base.ipkg. - In lib/Prelude/Chars.idr, use a List instead of a Vect - no need to know the size.

commita30a9c1475d83dcbdfc780488eedf2e80866744d authorReynir Reynisson <reynir@reynir.dk> dateSat 12 Oct 2013, 22:11 (13 years ago) parent53376fc
2 files changed+2−3
compare with master
unifiedsplit
lib/Prelude/Chars.idr+1−2 lib/base.ipkg+1−1
lib/Prelude/Chars.idr+1−2
@@ -1,7 +1,6 @@
11module Prelude.Char
22
33import Builtins
4−import Prelude.Vect
54
65isUpper : Char -> Bool
76isUpper x = x >= 'A' && x <= 'Z'
@@ -38,7 +37,7 @@ toLower x = if (isUpper x)
3837
3938isHexDigit : Char -> Bool
4039isHexDigit x = elem (toUpper x) hexChars where
41− hexChars : Vect 16 Char
40+ hexChars : List Char
4241 hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
4342 'A', 'B', 'C', 'D', 'E', 'F']
4443
lib/base.ipkg+1−1
@@ -7,7 +7,7 @@ modules = Builtins, Prelude, IO, System,
77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
88 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
99 Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
10− Prelude.Traversable,
10+ Prelude.Traversable, Prelude.Bits,
1111
1212 Network.Cgi,
1313 Debug.Trace,