Data.Metrology.Z

The Z datatype

data Z

data family Sing a

type SZ z

Defunctionalization symbols (these can be ignored)

type ZeroSym0

data SSym0 l

type SSym1 t

data PSym0 l

type PSym1 t

Conversions

zToInt

szToInt

Type-level operations

Arithmetic

type family Succ z :: Z

type family Pred z :: Z

type family Negate z :: Z

type family a #+ b :: Z

type family a #- b :: Z

type family a #* b :: Z

type family a #/ b :: Z

sSucc

sPred

sNegate

Comparisons

type family a < b :: Bool

type family NonNegative z :: Constraint

Synonyms for certain numbers

type One

type Two

type Three

type Four

type Five

type MOne

type MTwo

type MThree

type MFour

type MFive

sZero

sOne

sTwo

sThree

sFour

sFive

sMOne

sMTwo

sMThree

sMFour

sMFive

Deprecated synonyms

pZero

pOne

pTwo

pThree

pFour

pFive

pMOne

pMTwo

pMThree

pMFour

pMFive

pSucc

pPred