| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Basement.Nat
Synopsis
- type Nat = Natural
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer
- type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint)
- type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
- type family (a :: Natural) + (b :: Natural) :: Natural where ...
- type family (a :: Natural) * (b :: Natural) :: Natural where ...
- type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
- type family (a :: Natural) - (b :: Natural) :: Natural where ...
- type family CmpNat (a :: Natural) (b :: Natural) :: 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
A type synonym for Natural.
Prevously, this was an opaque data type, but it was changed to a type synonym.
Since: base-4.16.0.0
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
type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 #
Comparison (<=) of comparable types, as a constraint.
Since: base-4.16.0.0
type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 #
Comparison (<=) of comparable types, as a function.
Since: base-4.16.0.0
type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Natural) (b :: Natural) :: 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