Data.Type.Witness.Specific.PeanoNat

Documentation

data PeanoNatType t where

Constructors

ZeroType :: PeanoNatType 'Zero

SuccType :: PeanoNatType t -> PeanoNatType ('Succ t)

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

data GreaterEqual a b where

Constructors

ZeroGreaterEqual :: GreaterEqual a 'Zero

SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)

greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b

samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a

diff1GreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) b

peanoGreaterEqual :: PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)

addPeanoNatType :: PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b)

addZeroPeanoNatTypeEqual :: PeanoNatType a -> Add a 'Zero :~: a

succAddPeanoNatTypeEqual' :: forall a b. PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)

succAddPeanoNatTypeEqual :: forall a b. PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b)

addPeanoNatTypeGE :: PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a

data Greater a b where

Constructors

MkGreater :: GreaterEqual a b -> Greater ('Succ a) b

Instances

Countable (Greater 'Zero b)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

countPrevious :: Greater 'Zero b -> Maybe (Greater 'Zero b)

countMaybeNext :: Maybe (Greater 'Zero b) -> Maybe (Greater 'Zero b)

Empty (Greater 'Zero b)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

never :: Greater 'Zero b -> a

Finite (Greater 'Zero b)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

allValues :: [Greater 'Zero b]

assemble :: forall b0 f. Applicative f => (Greater 'Zero b -> f b0) -> f (Greater 'Zero b -> b0)

Searchable (Greater 'Zero b)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

search :: (Greater 'Zero b -> Maybe b0) -> Maybe b0

Eq (Greater 'Zero b)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

(==) :: Greater 'Zero b -> Greater 'Zero b -> Bool

(/=) :: Greater 'Zero b -> Greater 'Zero b -> Bool

greaterIndex :: Greater a b -> PeanoNatType b

peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b)