| Copyright | (C) 2017 mniip |
|---|---|
| License | MIT |
| Maintainer | mniip@mniip.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
GHC.TypeLits.Singletons
Description
- class NatSingleton (p :: Nat -> *) where
- data NatIsZero (n :: Nat) where
- data NatPeano (n :: Nat) where
- data NatTwosComp (n :: Nat) where
- TwosCompZero :: NatTwosComp 0
- TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + (2 * n))
- TwosCompx2p2 :: KnownNat n => NatTwosComp n -> NatTwosComp (2 + (2 * n))
- data NatBaseComp (p :: Nat -> *) (b :: Nat) (n :: Nat) where
- BaseCompZero :: NatBaseComp p b 0
- BaseCompxBp1p :: (KnownNat k, (1 + k) <= b, KnownNat n) => p k -> NatBaseComp p b n -> NatBaseComp p b ((1 + k) + (b * n))
- class PositiveSingleton (p :: Nat -> *) where
- data Unary (n :: Nat) where
- data PosBinary (n :: Nat) where
- data PosBase (p :: Nat -> *) (b :: Nat) (n :: Nat) where
- class ShowN (p :: Nat -> *) where
Natural number singletons
class NatSingleton (p :: Nat -> *) where Source #
A class of singletons capable of representing any KnownNat natural number.
Minimal complete definition
Methods
natSingleton :: KnownNat n => p n Source #
Instances
data NatPeano (n :: Nat) where Source #
A natural number is either 0 or a successor of another natural number.
data NatTwosComp (n :: Nat) where Source #
A natural number is either 0, or twice another natural number plus 1 or 2.
Constructors
| TwosCompZero :: NatTwosComp 0 | |
| TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + (2 * n)) | |
| TwosCompx2p2 :: KnownNat n => NatTwosComp n -> NatTwosComp (2 + (2 * n)) |
Instances
data NatBaseComp (p :: Nat -> *) (b :: Nat) (n :: Nat) where Source #
A natural number is either 0, or b times another natural number plus a digit in [1, b].
Constructors
| BaseCompZero :: NatBaseComp p b 0 | |
| BaseCompxBp1p :: (KnownNat k, (1 + k) <= b, KnownNat n) => p k -> NatBaseComp p b n -> NatBaseComp p b ((1 + k) + (b * n)) |
Instances
| ShowN p => ShowN (NatBaseComp p b) Source # | |
| (KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b) Source # | |
| ShowN p => Show (NatBaseComp p b n) Source # | |
Positive number singleton
class PositiveSingleton (p :: Nat -> *) where Source #
A class of singletons capable of representing postive KnownNat natural numbers.
Minimal complete definition
Methods
posSingleton :: KnownNat n => p (1 + n) Source #
Instances
data Unary (n :: Nat) where Source #
A positive number is either 1 or a successor of another positive number.
data PosBinary (n :: Nat) where Source #
A positive number is either 1, or twice another positive number plus 0 or 1.
data PosBase (p :: Nat -> *) (b :: Nat) (n :: Nat) where Source #
A positive number is either a digit in [1, b), or another positive number times b plus a digit in [0, b).