git.iko.soy/Idris-dev
on master help sign in
Fix imports and make hexVect local
9cbb5dbReynir Reynisson
lib/Prelude/Bits.idr+5−5
compare with master
unifiedsplit
@@ -1,18 +1,18 @@
1module Prelude.Bits
1module Prelude.Bits
2
2
3import Prelude.Strings
3import Prelude.Strings
4+import Prelude.Vect
4
5
5%access public
6%access public
6%default total
7%default total
7
8
8−private
9−hexVect : Vect 16 Char
10−hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
11− 'A', 'B', 'C', 'D', 'E', 'F']
12
9
13private
10private
14toHexDigit : Fin 16 -> Char
11toHexDigit : Fin 16 -> Char
15−toHexDigit n = index n hexVect
12+toHexDigit n = index n hexVect where
13+ hexVect : Vect 16 Char
14+ hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
15+ 'A', 'B', 'C', 'D', 'E', 'F']
16
16
17b8ToString : Bits8 -> String
17b8ToString : Bits8 -> String
18b8ToString c = pack [c1, c2] where
18b8ToString c = pack [c1, c2] where