-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathNonSIUnits.idr
275 lines (215 loc) · 6.61 KB
/
NonSIUnits.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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
module Quantities.NonSIUnits
import Quantities.FreeAbelianGroup
import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.SIDerivedQuantities
import Quantities.SIPrefixes
import Quantities.SIBaseUnits
import Quantities.SIDerivedUnits
%default total
%access public export
-- Based on http://en.wikipedia.org/wiki/Non-SI_units_mentioned_in_the_SI
Minute : ElemUnit Time
Minute = < one "min" equals 60 Second >
Min : ElemUnit Time
Min = Minute
Hour : ElemUnit Time
Hour = < one "h" equals 60 Minute >
H : ElemUnit Time
H = Hour
Day : ElemUnit Time
Day = < one "d" equals 24 Hour >
D : ElemUnit Time
D = Day
Week : ElemUnit Time
Week = < one "week" equals 7 Day >
-- Julian year
Year : ElemUnit Time
Year = < one "a" equals 365.25 Day >
JulianYear : ElemUnit Time
JulianYear = Year
A : ElemUnit Time
A = Year
Century : Unit Time
Century = hecto Year
Millenium : Unit Time
Millenium = kilo Year
Tonne : ElemUnit Mass
Tonne = < one "t" equals 1000 Kg >
T : ElemUnit Mass
T = Tonne
Degree : ElemUnit PlaneAngle
Degree = < one "deg" equals (pi / 180) Rad >
Deg : ElemUnit PlaneAngle
Deg = Degree
Arcmin : ElemUnit PlaneAngle
Arcmin = < one "arcmin" equals (1/60) Degree >
Arcsec : ElemUnit PlaneAngle
Arcsec = < one "arcsec" equals (1/60) Arcmin >
-- Ångström (Å)
Angstrom : ElemUnit Length
Angstrom = < one "angstrom" equals 0.1 (nano Metre) >
AstronomicalUnit : ElemUnit Length
AstronomicalUnit = < one "au" equals 149597870700 Metre >
Au : ElemUnit Length
Au = AstronomicalUnit
StandardGravity : ElemUnit Acceleration
--StandardGravity = < one "g_0" equals 9.80665 (Metre <//> (Second ^^ 2)) >
StandardGravity = defineAsMultipleOf "g_0" 9.80665 (Metre <//> (Second ^^ 2))
G_0 : ElemUnit Acceleration
G_0 = StandardGravity
RotationsPerMinute : Unit Frequency
RotationsPerMinute = One <//> Minute
Rpm : Unit Frequency
Rpm = RotationsPerMinute
-- Use this only for relative temparature! Not suitable for conversions of
-- absolute temperature!
Fahrenheit : ElemUnit Temperature
Fahrenheit = < one "dF" equals (5/9) K > -- °F
DF : ElemUnit Temperature
DF = Fahrenheit
Are : ElemUnit Area
Are = < one "are" equals 100 (Metre ^^ 2) >
Hectare : ElemUnit Area
Hectare = < one "ha" equals 1 ((hecto Metre) ^^ 2) >
Ha : ElemUnit Area
Ha = Hectare
Barn : ElemUnit Area
Barn = < one "b" equals 100 ((femto Metre) ^^ 2) >
B : ElemUnit Area
B = Barn
Litre : ElemUnit Volume
Litre = < one "l" equals 1 (milli (Metre ^^ 3)) >
Liter : ElemUnit Volume
Liter = Litre
L : ElemUnit Volume
L = Litre
Bar : ElemUnit Pressure
Bar = < one "bar" equals 100 (kilo Pascal) >
MillimetreOfMercury : ElemUnit Pressure
MillimetreOfMercury = < one "mmHg" equals 133.322 Pascal >
MmHg : ElemUnit Pressure
MmHg = MillimetreOfMercury
Calorie : ElemUnit Energy
Calorie = < one "cal" equals 4.18400 Joule >
ThermochemicalCalorie : ElemUnit Energy
ThermochemicalCalorie = Calorie
Cal : ElemUnit Energy
Cal = Calorie
-- Non-SI units whose values in SI must be determined experimentally
Electronvolt : ElemUnit Energy
Electronvolt = < one "eV" equals 1.60217653 (Ten ^^ -19 <**> Joule) >
EV : ElemUnit Energy
EV = Electronvolt
Dalton : ElemUnit Mass
Dalton = < one "Da" equals 1.66053886 (Ten ^^ -27 <**> Kilogram) >
Da : ElemUnit Mass
Da = Dalton
UnifiedAtomicMassUnit : ElemUnit Mass
UnifiedAtomicMassUnit = Dalton
U : ElemUnit Mass
U = Dalton
-- Atomic and natural units
ElementaryCharge : ElemUnit ElectricCharge
ElementaryCharge = < one "e" equals 1.60217653 (Ten ^^ -19 <**> Coulomb) >
E : ElemUnit ElectricCharge
E = ElementaryCharge
MassOfElectron : ElemUnit Mass
MassOfElectron = < one "m_e" equals 9.1093826 (Ten ^^ -31 <**> Kilogram) >
ElectronMass : ElemUnit Mass
ElectronMass = MassOfElectron
M_e : ElemUnit Mass
M_e = MassOfElectron
BohrRadius : ElemUnit Length
BohrRadius = < one "a_0" equals 0.5291772108 (Ten ^^ -10 <**> Metre) >
Bohr : ElemUnit Length
Bohr = BohrRadius
A_0 : ElemUnit Length
A_0 = BohrRadius
HartreeEnergy : ElemUnit Energy
HartreeEnergy = < one "E_h" equals 4.35974417 (Ten ^^ -18 <**> Joule) >
Hartree : ElemUnit Energy
Hartree = HartreeEnergy
E_h : ElemUnit Energy
E_h = HartreeEnergy
PlanckConstant : ElemUnit (Energy <*> Time)
PlanckConstant = < one "h" equals 6.62606957 (Joule <**> Second) >
H_ : ElemUnit (Energy <*> Time)
H_ = PlanckConstant
ReducedPlanckConstant : ElemUnit (Energy <*> Time)
ReducedPlanckConstant = < one "hBar" equals (1 / (2*pi)) (Joule <**> Second) >
HBar : ElemUnit (Energy <*> Time)
HBar = ReducedPlanckConstant
AtomicUnitOfTime : ElemUnit Time
AtomicUnitOfTime = < one "auOfTime" equals 1 (HBar <//> Hartree) >
AuOfTime : ElemUnit Time
AuOfTime = AtomicUnitOfTime
SpeedOfLight : ElemUnit Speed
SpeedOfLight = < one "c_0" equals 299792458 (Metre <//> Second) >
C_0 : ElemUnit Speed
C_0 = SpeedOfLight
NaturalUnitOfTime : ElemUnit Time
NaturalUnitOfTime = < one "nuOfTime" equals 1 (HBar <//> (M_e <**> (C_0 ^^ 2))) >
NuOfTime : ElemUnit Time
NuOfTime = NaturalUnitOfTime
LightSecond : ElemUnit Length
LightSecond = < one "ls" equals 1 (Second <**> SpeedOfLight) >
Ls : ElemUnit Length
Ls = LightSecond
LightMinute : ElemUnit Length
LightMinute = < one "lmin" equals 1 (Minute <**> SpeedOfLight) >
Lmin : ElemUnit Length
Lmin = LightMinute
LightHour : ElemUnit Length
LightHour = < one "lh" equals 1 (Hour <**> SpeedOfLight) >
Lh : ElemUnit Length
Lh = LightHour
LightDay : ElemUnit Length
LightDay = < one "ld" equals 1 (Day <**> SpeedOfLight) >
Ld : ElemUnit Length
Ld = LightDay
LightWeek : ElemUnit Length
LightWeek = < one "ld" equals 1 (Week <**> SpeedOfLight) >
Lw : ElemUnit Length
Lw = LightWeek
LightYear : ElemUnit Length
LightYear = < one "ly" equals 1 (Year <**> SpeedOfLight) >
Ly : ElemUnit Length
Ly = LightYear
-- Non-SI units associated with the CGS and the CGS-Gaussian system of units
Erg : Unit Energy
Erg = Ten ^^ -7 <**> Joule
Dyne : Unit Force'
Dyne = Ten ^^ -5 <**> Newton
Dyn : Unit Force'
Dyn = Dyne
Poise : Unit DynamicViscosity
Poise = Dyne <**> Second <//> (Centimetre ^^ 2)
P : Unit DynamicViscosity
P = Poise
Stokes : Unit KinematicViscosity
Stokes = Centimetre ^^ 2 <//> Second
St : Unit KinematicViscosity
St = Stokes
Stilb : Unit Luminance
Stilb = Candela <//> (Centimetre ^^ 2)
Sb : Unit Luminance
Sb = Stilb
Phot : Unit Illuminance
Phot = Candela <**> Steradian <//> (Centimetre ^^ 2)
Ph : Unit Illuminance
Ph = Phot
Gal : Unit Acceleration
Gal = Centimetre <//> (Second ^^ 2)
Maxwell : Unit MagneticFlux
Maxwell = Ten ^^ -8 <**> Weber
Mx : Unit MagneticFlux
Mx = Maxwell
Gauss : Unit MagneticFluxDensity
Gauss = Maxwell <//> (Centimetre ^^ 2)
G : Unit MagneticFluxDensity
G = Gauss
Oersted : ElemUnit MagneticFieldStrength
Oersted = < one "oe" equals (250 / pi) (Ampere <//> Metre) >
Oe : ElemUnit MagneticFieldStrength
Oe = Oersted