Data.Dimensions

Term-level combinators

(.+)

(.-)

(.*)

(./)

(.^)

(*.)

(.<)

(.>)

(.<=)

(.>=)

dimEq

dimNeq

nthRoot

dimSqrt

dimCubeRoot

unity

zero

dim

dimIn

(#)

dimOf

(%)

Type-level unit combinators

data u1 :* u2

data u1 :/ u2

data unit :^ power

data prefix :@ unit

class UnitPrefix prefix

Type-level dimensioned-quantity combinators

type family d1 (%*) d2 :: *

type family d1 (%/) d2 :: *

type family d (%^) z :: *

Creating new units

class Unit unit

type MkDim unit

type MkGenDim n unit

data Canonical

Scalars, the only built-in unit

data Number

type Scalar

scalar

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