| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Type.Data.Num.Unary.Proof
Synopsis
- data Nat x = Natural x => Nat
- data Pos x = 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)
- data AddZeroL x = (Zero :+: x) ~ x => AddZeroL
- addZeroL :: Nat x -> AddZeroL x
- data AddComm x y = (x :+: y) ~ (y :+: x) => AddComm
- addComm :: Nat x -> Nat y -> AddComm x y
- data AddAssoc x y z = (x :+: (y :+: z)) ~ ((x :+: y) :+: z) => AddAssoc
- addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z
- mulNat :: Nat x -> Nat y -> Nat (x :*: y)
- mulPos :: Pos x -> Pos y -> Pos (x :*: y)