| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Basement.Nat
Contents
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
class KnownNat (n :: Nat ) Source #
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 Source #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family (a :: Nat ) <=? (b :: Nat ) :: Bool where ... infix 4 Source #
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 Source #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat ) * (b :: Nat ) :: Nat where ... infixl 7 Source #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat ) ^ (b :: Nat ) :: Nat where ... infixr 8 Source #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat ) - (b :: Nat ) :: Nat where ... infixl 6 Source #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Nat ) (b :: Nat ) :: Ordering where ... Source #
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