Module
Type.Data.Peano
- Package
- purescript-typelevel-peano
- Repository
- csicar/purescript-typelevel-peano
Re-exports from Type.Data.Peano.Int
#Pos Source
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
#Neg Source
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
#ParseInt Source
#ProductInt Source
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
#SumInt Source
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)
Re-exports from Type.Data.Peano.Nat
#Succ Source
data Succ :: Nat -> Nat
Represents Successor of a Nat: (Succ a) ^= 1 + a
Instances
(IsNat a) => IsNat (Succ a)
(SumNat a b c) => SumNat (Succ a) b (Succ c)
ProductNat (Succ Z) a a
1 * a = a
(ProductNat a b ab, SumNat ab b result) => ProductNat (Succ a) b result
(1 + a) * b = b + a * b
ExponentiationNat a Z (Succ Z)
(ExponentiationNat a b ab, ProductNat ab a result) => ExponentiationNat a (Succ b) result
(CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
IsZeroNat (Succ a) False
#CompareNat Source
class CompareNat (a :: Nat) (b :: Nat) (ord :: Ordering) | a b -> ord
Instances
CompareNat a a EQ
CompareNat Z a LT
CompareNat a Z GT
(CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
#ExponentiationNat Source
class ExponentiationNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c
Instances
ExponentiationNat a Z (Succ Z)
(ExponentiationNat a b ab, ProductNat ab a result) => ExponentiationNat a (Succ b) result
#ParseNat Source
class ParseNat (sym :: Symbol) (nat :: Nat) | nat -> sym, sym -> nat
Parses a Nat from a Symbol
ParseNat "2" ~> (Succ (Succ Z))
ParseNat "1283" ~> (Succ (...))
Instances
ParseNat "0" Z
ParseNat "1" (Succ Z)
ParseNat "2" (Succ (Succ Z))
ParseNat "3" (Succ (Succ (Succ Z)))
ParseNat "4" (Succ (Succ (Succ (Succ Z))))
ParseNat "5" (Succ (Succ (Succ (Succ (Succ Z)))))
ParseNat "6" (Succ (Succ (Succ (Succ (Succ (Succ Z))))))
ParseNat "7" (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))
ParseNat "8" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))
ParseNat "9" (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))))
(ParseNat head msd, Cons head tail sym, Length tail symLength, ExponentiationNat D10 symLength offset, ProductNat offset msd high, ParseNat tail lower, SumNat high lower res) => ParseNat sym res
#ProductNat Source
class ProductNat (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c
a * b = c
Instances
ProductNat Z a Z
0 * a = 0
ProductNat (Succ Z) a a
1 * a = a
(ProductNat a b ab, SumNat ab b result) => ProductNat (Succ a) b result
(1 + a) * b = b + a * b
#powNat Source
powNat :: forall c b a. ExponentiationNat a b c => NProxy a -> NProxy b -> NProxy c
> powNat d2 d3
8 -- : NProxy D8
a raised to the power of b a^b = c
reflect a type-level Int to a value-level Int