tfp-1.0: Type-level integers, booleans, lists using type families

Safe HaskellSafe-Inferred
LanguageHaskell2010

Type.Data.Num.Decimal.Digit.Proof

Documentation

data Nat d Source

Constructors

C d => Nat 

data Pos d Source

Constructors

Pos d => Pos 

data UnaryNat d Source

Constructors

Natural (ToUnary d) => UnaryNat 

unaryNat :: C d => UnaryNat d Source

unaryNatImpl :: Nat d -> Nat (ToUnary d) Source

data UnaryPos d Source

Constructors

Positive (ToUnary d) => UnaryPos 

unaryPos :: Pos d => UnaryPos d Source

unaryPosImpl :: Pos d -> Pos (ToUnary d) Source