Data.Type.Witness.Specific.Natural

Documentation

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

type (<=) (x :: k) (y :: k) = (x <=? y) ~ 'True infix 4

Comparison (<=) of comparable types, as a constraint.

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

type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (a :: Natural) :: Natural where ...

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

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

data NaturalType bn where

Constructors

MkNaturalType :: KnownNat bn => NaturalType bn

Instances

TestEquality NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

testEquality :: forall (a :: k) (b :: k). NaturalType a -> NaturalType b -> Maybe (a :~: b)

TestOrder NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

testCompare :: forall (a :: k) (b :: k). NaturalType a -> NaturalType b -> WOrdering a b

Representative NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

getRepWitness :: Subrepresentative NaturalType NaturalType

WitnessValue NaturalType

Defined in Data.Type.Witness.Specific.Natural

Associated Types

type WitnessValueType NaturalType

Methods

witnessToValue :: forall (t :: k). NaturalType t -> WitnessValueType NaturalType

valueToWitness :: WitnessValueType NaturalType -> (forall (t :: k). NaturalType t -> r) -> r

KnownNat bn => Is NaturalType (bn :: Nat)

Defined in Data.Type.Witness.Specific.Natural

Methods

representative :: NaturalType bn

Show (NaturalType bn)

Defined in Data.Type.Witness.Specific.Natural

Methods

showsPrec :: Int -> NaturalType bn -> ShowS

show :: NaturalType bn -> String

showList :: [NaturalType bn] -> ShowS

AllConstraint Show NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

allConstraint :: forall (t :: kt). Dict (Show (NaturalType t))

type WitnessValueType NaturalType

Defined in Data.Type.Witness.Specific.Natural

type WitnessValueType NaturalType = Natural

zeroNaturalType :: NaturalType 0

succNaturalType :: NaturalType a -> NaturalType (a + 1)

addNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a + b)

multiplyNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a * b)

type family PeanoToNatural pn where ...

Equations

PeanoToNatural 'Zero = 0

PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1

peanoToNaturalType :: PeanoNatType pn -> NaturalType (PeanoToNatural pn)