Type.Data.Peano.Int.Definition

data Int

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

Instances

• (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

Instances

• (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)

Constructors

• IProxy

Instances

• (IsInt i) => Show (IProxy i)

class IsInt (i :: Int)  where

Members

• reflectInt :: forall proxy. proxy i -> Int

  reflect a type-level Int to a value-level Int

  reflectInt (Proxy  :: _ N10) = -10
  reflectInt (IProxy :: _ N10) = -10
  

Instances

• (IsNat n) => IsInt (Pos n)
• (IsNat n) => IsInt (Neg n)

showInt :: forall proxy i. IsInt i => proxy i -> String

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

Instances

• (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 proxy a b c. SumInt a b c => proxy a -> proxy b -> proxy 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

Instances

• Inverse (Pos Z) (Pos Z)
• Inverse (Pos a) (Neg a)
• Inverse (Neg Z) (Pos Z)
• Inverse (Neg a) (Pos a)

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

Instances

• (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 proxy a b c. ProductInt a b c => proxy a -> proxy b -> proxy c

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

Instances

• (IsZeroNat a isZero) => IsZeroInt (Pos a) isZero
• (IsZeroNat a isZero) => IsZeroInt (Neg a) isZero