basement-0.0.16: Foundation scrap box of array & string
Safe HaskellSafe-Inferred
LanguageHaskell2010

Basement.Nat

Synopsis

Documentation

type Nat = Natural #

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

class KnownNat (n :: Nat) #

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

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer #

Since: base-4.7.0.0

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 #

natValInt :: forall n proxy. (KnownNat n, NatWithinBound Int n) => proxy n -> Int 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

Instances details
type NatNumMaxBound Int16 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int16 = 32767
type NatNumMaxBound Int32 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int32 = 2147483647
type NatNumMaxBound Int64 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int64 = 9223372036854775807
type NatNumMaxBound Int8 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int8 = 127
type NatNumMaxBound Word16 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word16 = 65535
type NatNumMaxBound Word32 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word32 = 4294967295
type NatNumMaxBound Word64 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word64 = 18446744073709551615
type NatNumMaxBound Word8 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Char7 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word128 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word128 = 340282366920938463463374607431768211455
type NatNumMaxBound Word256 Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935
type NatNumMaxBound Char Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Char = 1114111
type NatNumMaxBound Int Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word Source # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound (Zn n) Source # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn n) = n
type NatNumMaxBound (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn64 n) = n
type NatNumMaxBound (CountOf x) Source # 
Instance details

Defined in Basement.Types.OffsetSize

type NatNumMaxBound (Offset x) Source # 
Instance details

Defined in Basement.Types.OffsetSize

Constraint

type family NatInBoundOf ty n where ... Source #

Check if a Nat is in bounds of another integral / natural types

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

Equations

NatWithinBound ty n = If (NatInBoundOf ty n) (() ~ ()) (TypeError ((('Text "Natural " ':<>: 'ShowType n) ':<>: 'Text " is out of bounds for ") ':<>: 'ShowType ty))