Module

Type.Data.Peano.Int.Definition

data Int :: Type

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

(IsNat n) => IsInt (Pos n)
(SumInt (Pos a) (Pos b) (Pos c')) => SumInt (Pos (Succ a)) (Pos b) (Pos (Succ c'))
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
SumInt (Pos Z) (Pos b) (Pos b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)
Inverse (Pos Z) (Pos Z)
Inverse (Pos a) (Neg a)
Inverse (Neg Z) (Pos Z)
Inverse (Neg a) (Pos a)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
ProductInt (Pos Z) a (Pos Z)
ProductInt (Pos (Succ Z)) a a
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(ProductInt (Pos a) b ab, SumInt ab b result) => ProductInt (Pos (Succ a)) b result
(IsZeroNat a isZero) => IsZeroInt (Pos a) isZero

data Neg :: Nat -> Int

Represents a negative number

Neg (Succ Z) ^= - 1

(IsNat n) => IsInt (Neg n)
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
(SumInt (Neg a) (Neg b) (Neg c')) => SumInt (Neg (Succ a)) (Neg b) (Neg (Succ c'))
SumInt (Neg Z) (Neg b) (Neg b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)
Inverse (Pos a) (Neg a)
Inverse (Neg Z) (Pos Z)
Inverse (Neg a) (Pos a)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(IsZeroNat a isZero) => IsZeroInt (Neg a) isZero

data IProxy (i :: Int)

class IsInt (i :: Int)  where

reflectInt :: IProxy i -> Int
reflect a type-level Int to a value-level Int
```
reflectInt (undefined :: IProxy N10) = -10
```

class SumInt (a :: Int) (b :: Int) (c :: Int) | a b -> c

(SumInt (Pos a) (Pos b) (Pos c')) => SumInt (Pos (Succ a)) (Pos b) (Pos (Succ c'))
(SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
(SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
(SumInt (Neg a) (Neg b) (Neg c')) => SumInt (Neg (Succ a)) (Neg b) (Neg (Succ c'))
SumInt (Pos Z) (Pos b) (Pos b)
SumInt (Neg Z) (Neg b) (Neg b)
SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
SumInt (Pos a) (Neg Z) (Pos a)
SumInt (Neg Z) (Pos a) (Pos a)

plus :: forall c b a. SumInt a b c => IProxy a -> IProxy b -> IProxy c

class Inverse (a :: Int) (b :: Int) | a -> b, b -> a

Invert the sign of a value (except for 0, which always stays positive)

Inverse (Pos (Succ Z)) ~> Neg (Succ Z)
Inverse (Pos Z) ~> Pos Z

class ProductInt (a :: Int) (b :: Int) (c :: Int) | a b -> c

(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
ProductInt (Pos Z) a (Pos Z)
ProductInt (Pos (Succ Z)) a a
(ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
(ProductInt (Pos a) b ab, SumInt ab b result) => ProductInt (Pos (Succ a)) b result

prod :: forall c b a. ProductInt a b c => IProxy a -> IProxy b -> IProxy c

class IsZeroInt (int :: Int) (isZero :: Boolean) | int -> isZero

Modules: Type.Data.Peano; Type.Data.Peano.Int; Type.Data.Peano.Int.Definition; Type.Data.Peano.Int.Parse; Type.Data.Peano.Int.TypeAliases; Type.Data.Peano.Nat; Type.Data.Peano.Nat.Definition; Type.Data.Peano.Nat.Parse; Type.Data.Peano.Nat.TypeAliases