| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Basement.Nat
Synopsis
- data Nat
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer
- type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
- natValNatural :: forall n proxy. KnownNat n => proxy n -> Natural
- natValInt :: forall n proxy. (KnownNat n, NatWithinBound Int n) => proxy n -> Int
- natValInt8 :: forall n proxy. (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8
- natValInt16 :: forall n proxy. (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16
- natValInt32 :: forall n proxy. (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32
- natValInt64 :: forall n proxy. (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64
- natValWord :: forall n proxy. (KnownNat n, NatWithinBound Word n) => proxy n -> Word
- natValWord8 :: forall n proxy. (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8
- natValWord16 :: forall n proxy. (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16
- natValWord32 :: forall n proxy. (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32
- natValWord64 :: forall n proxy. (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64
- type family NatNumMaxBound ty :: Nat
- type family NatInBoundOf ty n where ...
- type family NatWithinBound ty (n :: Nat) where ...
Documentation
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
Minimal complete definition
natSing
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True infix 4 #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
Nat convertion
natValNatural :: forall n proxy. KnownNat n => proxy n -> Natural Source #
natValInt8 :: forall n proxy. (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8 Source #
natValInt16 :: forall n proxy. (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16 Source #
natValInt32 :: forall n proxy. (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32 Source #
natValInt64 :: forall n proxy. (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64 Source #
natValWord :: forall n proxy. (KnownNat n, NatWithinBound Word n) => proxy n -> Word Source #
natValWord8 :: forall n proxy. (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8 Source #
natValWord16 :: forall n proxy. (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16 Source #
natValWord32 :: forall n proxy. (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32 Source #
natValWord64 :: forall n proxy. (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64 Source #
Maximum bounds
type family NatNumMaxBound ty :: Nat Source #
Get Maximum bounds of different Integral / Natural types related to Nat
Instances
Constraint
type family NatInBoundOf ty n where ... Source #
Check if a Nat is in bounds of another integral / natural types
Equations
| NatInBoundOf Integer n = 'True | |
| NatInBoundOf Natural n = 'True | |
| NatInBoundOf ty n = n <=? NatNumMaxBound ty |
type family NatWithinBound ty (n :: Nat) where ... Source #
Constraint to check if a natural is within a specific bounds of a type.
i.e. given a Nat n, is it possible to convert it to ty without losing information