tfp-1.0.2: Type-level integers, booleans, lists using type families
Safe HaskellSafe-Inferred
LanguageHaskell2010

Type.Data.Num.Unary.Proof

Synopsis

Documentation

data Nat x Source #

Constructors

Natural x => Nat 

data Pos x Source #

Constructors

Positive x => Pos 

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 #

data AddZeroL x Source #

Constructors

(Zero :+: x) ~ x => AddZeroL 

data AddComm x y Source #

Constructors

(x :+: y) ~ (y :+: x) => AddComm 

addComm :: Nat x -> Nat y -> AddComm x y Source #

The proof is pretty expensive. For proving (x:+:y ~ y:+:x) we need about x*y reduction steps.

data AddAssoc x y z Source #

Constructors

(x :+: (y :+: z)) ~ ((x :+: y) :+: z) => AddAssoc 

addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z Source #

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

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