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

Safe HaskellSafe-Inferred
LanguageHaskell2010

Type.Data.Num.Unary.Proof

Documentation

data Nat x Source

Constructors

Natural x => Nat 

data Pos x Source

Constructors

Positive x => Pos 

natFromPos :: Pos x -> Nat x Source

addNat :: Nat x -> Nat y -> Nat (x :+: y) Source

addPosL :: Pos x -> Nat y -> Pos (x :+: y) Source

addPosR :: Nat x -> Pos y -> Pos (x :+: y) Source

mulNat :: Nat x -> Nat y -> Nat (x :*: y) Source

mulPos :: Pos x -> Pos y -> Pos (x :*: y) Source