-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathImperialUnits.idr
206 lines (150 loc) · 3.97 KB
/
ImperialUnits.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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
module Quantities.ImperialUnits
import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.SIPrefixes
import Quantities.SIBaseUnits
import Quantities.SIDerivedQuantities
import Quantities.NonSIUnits
%default total
%access public export
-- Based on http://en.wikipedia.org/wiki/Imperial_units
-- Length
Thou : ElemUnit Length
Thou = < one "th" equals 25.4 (micro Metre) >
Th : ElemUnit Length
Th = Thou
Inch : ElemUnit Length
Inch = < one "in" equals 2.54 Centimetre >
In_ : ElemUnit Length
In_ = Inch
Foot : ElemUnit Length
Foot = < one "ft" equals 12 Inch >
Ft : ElemUnit Length
Ft = Foot
Yard : ElemUnit Length
Yard = < one "yd" equals 3 Foot >
Yd : ElemUnit Length
Yd = Yard
Chain : ElemUnit Length
Chain = < one "ch" equals 22 Yard >
Ch : ElemUnit Length
Ch = Chain
Furlong : ElemUnit Length
Furlong = < one "fur" equals 10 Chain >
Fur : ElemUnit Length
Fur = Furlong
Mile : ElemUnit Length
Mile = < one "mi" equals 1760 Yard >
Mi : ElemUnit Length
Mi = Mile
League : ElemUnit Length
League = < one "lea" equals 3 Mile >
Lea : ElemUnit Length
Lea = League
-- Maritime units
Fathom : ElemUnit Length
Fathom = < one "ftm" equals 6.08 Foot >
Ftm : ElemUnit Length
Ftm = Fathom
Cable : ElemUnit Length
Cable = < one "cable" equals 608 Foot >
NauticalMile : ElemUnit Length
NauticalMile = < one "nmi" equals 1852 Metre >
Nmi : ElemUnit Length
Nmi = NauticalMile
-- Gunter's survey units
Link : ElemUnit Length
Link = < one "link" equals (1/100) Chain >
Rod : ElemUnit Length
Rod = < one "rod" equals (1/4) Chain >
-- Speed
Knot : ElemUnit Speed
Knot = < one "kn" equals 1 (NauticalMile <//> Hour) >
Kn : ElemUnit Speed
Kn = Knot
-- Area
Perch : ElemUnit Area
Perch = < one "perch" equals 1 (Rod ^^ 2) >
Rood : ElemUnit Area
Rood = < one "rood" equals 1 (Furlong <**> Rod) >
Acre : ElemUnit Area
Acre = < one "acre" equals 1 (Furlong <**> Chain) >
-- Volume
FluidOunce : ElemUnit Volume
FluidOunce = < one "floz" equals 28.4130625 (milli $ (deci Metre) ^^ 3) >
Floz : ElemUnit Volume
Floz = FluidOunce
Gill : ElemUnit Volume
Gill = < one "gi" equals 5 FluidOunce >
Gi : ElemUnit Volume
Gi = Gill
Pint : ElemUnit Volume
Pint = < one "pt" equals 20 FluidOunce >
Pt : ElemUnit Volume
Pt = Pint
Quart : ElemUnit Volume
Quart = < one "qt" equals 40 FluidOunce >
Qt : ElemUnit Volume
Qt = Quart
Gallon : ElemUnit Volume
Gallon = < one "gal" equals 160 FluidOunce >
Gal : ElemUnit Volume
Gal = Gallon
-- British apothecaries' volume measures
Minim : ElemUnit Volume
Minim = < one "min" equals 59.1938802083 (micro $ (deci Metre) ^^ 3) >
Min : ElemUnit Volume
Min = Minim
FluidScruple : ElemUnit Volume
FluidScruple = < one "fls" equals 20 Minim >
Fls : ElemUnit Volume
Fls = FluidScruple
FluidDrachm : ElemUnit Volume
FluidDrachm = < one "fldr" equals 3 FluidScruple >
Fldr : ElemUnit Volume
Fldr = FluidDrachm
-- Mass
Pound : ElemUnit Mass
Pound = < one "lb" equals 453.59237 Gram >
Lb : ElemUnit Mass
Lb = Pound
Grain : ElemUnit Mass
Grain = < one "gr" equals (1/7000) Pound >
Gr : ElemUnit Mass
Gr = Grain
Drachm : ElemUnit Mass
Drachm = < one "dr" equals (1/256) Pound >
Dr : ElemUnit Mass
Dr = Drachm
Ounce : ElemUnit Mass
Ounce = < one "oz" equals (1/16) Pound >
Oz : ElemUnit Mass
Oz = Ounce
Stone : ElemUnit Mass
Stone = < one "st" equals 14 Pound >
St : ElemUnit Mass
St = Stone
Quarter : ElemUnit Mass
Quarter = < one "qtr" equals 28 Pound >
Qtr : ElemUnit Mass
Qtr = Quarter
Hundredweight : ElemUnit Mass
Hundredweight = < one "cwt" equals 112 Pound >
Cwt : ElemUnit Mass
Cwt = Hundredweight
Ton : ElemUnit Mass
Ton = < one "ton" equals 2240 Pound >
-- Energy
FootPound : ElemUnit Energy
FootPound = < one "ftlb" equals 1 (Foot <**> Pound <**> G_0) >
Ftlb : ElemUnit Energy
Ftlb = FootPound
-- Power
MechanicalHorsepower : ElemUnit Power
MechanicalHorsepower = < one "hp" equals 550 (FootPound <//> Second) >
ImperialHorsepower : ElemUnit Power
ImperialHorsepower = MechanicalHorsepower
Horsepower : ElemUnit Power
Horsepower = MechanicalHorsepower
Hp : ElemUnit Power
Hp = MechanicalHorsepower