-
Notifications
You must be signed in to change notification settings - Fork 11
/
Information.idr
64 lines (48 loc) · 1.36 KB
/
Information.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
module Quantities.Information
import Quantities.Core
%default total
%access public export
Information : Dimension
Information = MkDimension "Information"
Bit : ElemUnit Information
Bit = MkElemUnit "bit" 1
Byte : ElemUnit Information
Byte = < one "byte" equals 8 Bit >
-- Binary prefixes for multiples of bits/bytes
-- Based on http://en.wikipedia.org/wiki/Binary_prefix
twoToTheTen : String -> Nat -> ElemUnit q -> ElemUnit q
twoToTheTen pre power (MkElemUnit name f) =
< one (pre ++ name) equals (pow 1024.0 power) (MkElemUnit name f) >
kibi : ElemUnit q -> ElemUnit q
kibi = twoToTheTen "kibi" 1
ki : ElemUnit q -> ElemUnit q
ki = kibi
mebi : ElemUnit q -> ElemUnit q
mebi = twoToTheTen "mebi" 2
mi : ElemUnit q -> ElemUnit q
mi = mebi
gibi : ElemUnit q -> ElemUnit q
gibi = twoToTheTen "gibi" 3
gi : ElemUnit q -> ElemUnit q
gi = gibi
tebi : ElemUnit q -> ElemUnit q
tebi = twoToTheTen "tebi" 4
ti : ElemUnit q -> ElemUnit q
ti = tebi
pebi : ElemUnit q -> ElemUnit q
pebi = twoToTheTen "pebi" 5
pi : ElemUnit q -> ElemUnit q
pi = pebi
exbi : ElemUnit q -> ElemUnit q
exbi = twoToTheTen "exbi" 6
ei : ElemUnit q -> ElemUnit q
ei = exbi
zebi : ElemUnit q -> ElemUnit q
zebi = twoToTheTen "zebi" 7
zi : ElemUnit q -> ElemUnit q
zi = zebi
yobi : ElemUnit q -> ElemUnit q
yobi = twoToTheTen "yobi" 8
yi : ElemUnit q -> ElemUnit q
yi = yobi
-- Please Note: kibi byte /= kilo byte