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

Safe HaskellSafe
LanguageHaskell2010

Type.Data.Num.Unary.Proof

Documentation

data Nat x #

Constructors

Natural x => Nat 

data Pos x #

Constructors

Positive x => Pos 

natFromPos :: Pos x -> Nat x #

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

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

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

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

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