Module
Type.Data.Peano.Nat
- Package
- purescript-typelevel-peano
- Repository
- csicar/purescript-typelevel-peano
Re-exports from Type.Data.Peano.Nat.Definition
#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
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
Pred (Succ a) a
#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
#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
#powNat Source
powNat :: forall proxy a b c. ExponentiationNat a b c => proxy a -> proxy b -> proxy c
> powNat d2 d3
8 -- : NProxy D8
a raised to the power of b a^b = c
#mulNat Source
mulNat :: forall proxy a b c. ProductNat a b c => proxy a -> proxy b -> proxy c
Re-exports from Type.Data.Peano.Nat.Parse
#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
0 * a = 0