Safe Haskell	None
Language	GHC2021

Data.PeanoNat

Synopsis

data PeanoNat
- = Zero
- | Succ PeanoNat
addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
type family Add (a :: PeanoNat) (b :: PeanoNat) :: PeanoNat where ...
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
peanoToNatural :: PeanoNat -> Natural
naturalToPeano :: Natural -> PeanoNat
type family PeanoToNatural (pn :: PeanoNat) :: Nat where ...
type family ListLength (l :: [k]) :: PeanoNat where ...

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 :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (a :~: b) #

TestOrder PeanoNatType Source #

Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

testCompare :: forall (a :: PeanoNat) (b :: PeanoNat). 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
Instance details Defined in Data.Type.Witness.Specific.PeanoNat type WitnessValueType PeanoNatType = PeanoNat

Methods

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

valueToWitness :: WitnessValueType PeanoNatType -> (forall (t :: PeanoNat). 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 :: PeanoNat) (b :: PeanoNat) :: PeanoNat 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 :: PeanoNat) :: Nat where ... Source #

Equations

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

type family ListLength (l :: [k]) :: PeanoNat where ... Source #

Equations

ListLength ('[] :: [k]) = 'Zero
ListLength (_1 ': aa :: [k]) = 'Succ (ListLength aa)