Data.Metrology

Term-level combinators

(|+|)

(|-|)

(|*|)

(|/|)

(*|)

(|*)

(/|)

(|/)

(|^)

(|^^)

(|<|)

(|>|)

(|<=|)

(|>=|)

(|==|)

(|/=|)

qApprox

qNapprox

qSq

qCube

qSqrt

qCubeRoot

nthRoot

Nondimensional units, conversion between quantities and numeric values

unity

zero

redim

convert

numIn

(#)

(##)

quOf

(%)

(%%)

defaultLCSU

fromDefaultLCSU

constant

Type-level unit combinators

data u1 :* u2

data u1 :/ u2

data unit :^ power

data prefix :@ unit

class UnitPrefix prefix

Type-level quantity combinators

type family d1 %* d2 :: *

type family d1 %/ d2 :: *

type family d %^ z :: *

Creating quantity types

data Qu a lcsu n

type MkQu_D dim

type MkQu_DLN dim

type MkQu_U unit

type MkQu_ULN unit

Creating new dimensions

class Dimension dim

Creating new units

class Unit unit

data Canonical

Scalars, the only built-in unit

data Dimensionless

data Number

type Scalar

scalar

LCSUs (locally coherent system of units)

type family MkLCSU pairs

data LCSU star

type family DefaultUnitOfDim dim :: *

Validity checks and assertions

type family CompatibleUnit lcsu unit :: Constraint

type family CompatibleDim lcsu dim :: Constraint

type family ConvertibleLCSUs_D dim l1 l2 :: Constraint

type family DefaultConvertibleLCSU_D dim l :: Constraint

type family DefaultConvertibleLCSU_U unit l :: Constraint

Type-level integers

data Z

type family Succ z :: Z

type family Pred z :: Z

type family a #+ b :: Z

type family a #- b :: Z

type family a #* b :: Z

type family a #/ b :: Z

type family NegZ z :: Z

Synonyms for small numbers

type One

type Two

type Three

type Four

type Five

type MOne

type MTwo

type MThree

type MFour

type MFive

Term-level singletons

pZero

pOne

pTwo

pThree

pFour

pFive

pMOne

pMTwo

pMThree

pMFour

pMFive

pSucc

pPred

Internal definitions