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

Data.Type.Witness.Specific.PeanoNat

Documentation

data PeanoNatType t where Source #

Constructors

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

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

data GreaterEqual a b where Source #

Constructors

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

greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b Source #

samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a Source #

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

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

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

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

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

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

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

data Greater a b where Source #

Constructors

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

Instances

Instances details
Countable (Greater 'Zero b) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

never :: Greater 'Zero b -> a #

Finite (Greater 'Zero b) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

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

Eq (Greater 'Zero b) Source # 
Instance details

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 Source #

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