Module

Type.Data.Peano.Int.Definition

Package
purescript-typelevel-peano
Repository
csicar/purescript-typelevel-peano

#Int Source

data Int :: Type

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0

#Pos Source

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

Instances

#Neg Source

data Neg :: Nat -> Int

Represents a negative number

Neg (Succ Z) ^= - 1

Instances

#IProxy Source

data IProxy (i :: Int)

Instances

#IsInt Source

class IsInt (i :: Int)  where

Members

  • reflectInt :: IProxy i -> Int

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

    reflectInt (undefined :: IProxy N10) = -10
    

Instances

#SumInt Source

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

Instances

#plus Source

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

#Inverse Source

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 Source

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

Instances

#prod Source

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

#IsZeroInt Source

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

Instances