witness-0.7: values that witness types
Safe HaskellNone
LanguageGHC2021

Data.Type.Witness.Specific.Natural

Synopsis

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 :: 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 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.

Previously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

data NaturalType (bn :: Nat) where Source #

Constructors

MkNaturalType :: forall (bn :: Nat). KnownNat bn => NaturalType bn 

Instances

Instances details
TestEquality NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

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

TestOrder NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

testCompare :: forall (a :: Nat) (b :: Nat). NaturalType a -> NaturalType b -> WOrdering a b Source #

Representative NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

getRepWitness :: Subrepresentative NaturalType NaturalType Source #

WitnessValue NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Associated Types

type WitnessValueType NaturalType 
Instance details

Defined in Data.Type.Witness.Specific.Natural

type WitnessValueType NaturalType = Natural

Methods

witnessToValue :: forall (t :: Nat). NaturalType t -> WitnessValueType NaturalType Source #

valueToWitness :: WitnessValueType NaturalType -> (forall (t :: Nat). NaturalType t -> r) -> r Source #

KnownNat bn => Is NaturalType (bn :: Nat) Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

representative :: NaturalType bn Source #

AllConstraint Show NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

allConstraint :: forall (t :: Nat). Dict (Show (NaturalType t)) Source #

Show (NaturalType bn) Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

Methods

showsPrec :: Int -> NaturalType bn -> ShowS #

show :: NaturalType bn -> String #

showList :: [NaturalType bn] -> ShowS #

type WitnessValueType NaturalType Source # 
Instance details

Defined in Data.Type.Witness.Specific.Natural

type WitnessValueType NaturalType = Natural

zeroNaturalType :: NaturalType 0 Source #

succNaturalType :: forall (a :: Nat). NaturalType a -> NaturalType (a + 1) Source #

addNaturalType :: forall (a :: Nat) (b :: Nat). NaturalType a -> NaturalType b -> NaturalType (a + b) Source #

multiplyNaturalType :: forall (a :: Nat) (b :: Nat). NaturalType a -> NaturalType b -> NaturalType (a * b) Source #

type family PeanoToNatural (pn :: PeanoNat) :: Nat where ... Source #

Equations

PeanoToNatural 'Zero = 0 
PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1 

peanoToNaturalType :: forall (pn :: PeanoNat). PeanoNatType pn -> NaturalType (PeanoToNatural pn) Source #