Module

Type.Data.Peano.Int.Definition

#Int 

data Int

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

#Pos 

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

Instances

#Neg 

data Neg :: Nat -> Int

Represents a negative number

Neg (Succ Z) ^= - 1

Instances

#IProxy 

data IProxy (i :: Int)

Constructors

Instances

#IsInt 

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

#showInt 

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

#SumInt 

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

Instances

#plus 

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

#Inverse 

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

#ProductInt 

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

Instances

#prod 

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

#IsZeroInt 

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

Instances

Modules