Data.PeanoNat

Documentation

data PeanoNat

Inductive natural numbers.

Constructors

Zero

Succ PeanoNat

Instances

TestEquality PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

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

TestOrder PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

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

Representative PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

getRepWitness :: Subrepresentative PeanoNatType PeanoNatType

WitnessValue PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Associated Types

type WitnessValueType PeanoNatType

Methods

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

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

Is PeanoNatType 'Zero

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType 'Zero

Is PeanoNatType n => Is PeanoNatType ('Succ n :: PeanoNat)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType ('Succ n)

type WitnessValueType PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

type WitnessValueType PeanoNatType = PeanoNat

addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat

type family Add a b where ...

Equations

Add 'Zero b = b

Add ('Succ a) b = 'Succ (Add a b)

subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat

subtractFromPeanoNat a b = b - a

multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat

peanoToNatural :: PeanoNat -> Natural

naturalToPeano :: Natural -> PeanoNat

type family PeanoToNatural pn where ...

Equations

PeanoToNatural 'Zero = 0

PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1

type family ListLength l where ...

Equations

ListLength '[] = 'Zero

ListLength (a ': aa) = 'Succ (ListLength aa)