witness-0.6.2: values that witness types
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.PeanoNat

Synopsis

Documentation

data PeanoNat Source #

Inductive natural numbers.

Constructors

Zero 
Succ PeanoNat 

Instances

Instances details
TestEquality PeanoNatType Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

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

TestOrder PeanoNatType Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

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

Representative PeanoNatType Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

getRepWitness :: Subrepresentative PeanoNatType PeanoNatType Source #

WitnessValue PeanoNatType Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Associated Types

type WitnessValueType PeanoNatType Source #

Methods

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

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

Is PeanoNatType 'Zero Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType 'Zero Source #

Is PeanoNatType n => Is PeanoNatType ('Succ n :: PeanoNat) Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType ('Succ n) Source #

type WitnessValueType PeanoNatType Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

type WitnessValueType PeanoNatType = PeanoNat

addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat Source #

type family Add a b where ... Source #

Equations

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

subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat Source #

subtractFromPeanoNat a b = b - a

multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat Source #

peanoToNatural :: PeanoNat -> Natural Source #

naturalToPeano :: Natural -> PeanoNat Source #

type family PeanoToNatural pn where ... Source #

Equations

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

type family ListLength l where ... Source #

Equations

ListLength '[] = 'Zero 
ListLength (a ': aa) = 'Succ (ListLength aa)