witness-0.7: values that witness types

Safe Haskell	None
Language	GHC2021

Data.Type.Witness.Specific.PeanoNat

Documentation

data PeanoNatType (t :: PeanoNat) where Source #

Constructors

ZeroType :: PeanoNatType 'Zero
SuccType :: forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1)

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

data GreaterEqual (a :: PeanoNat) (b :: PeanoNat) where Source #

Constructors

ZeroGreaterEqual :: forall (a :: PeanoNat). GreaterEqual a 'Zero
SuccGreaterEqual :: forall (a1 :: PeanoNat) (b1 :: PeanoNat). GreaterEqual a1 b1 -> GreaterEqual ('Succ a1) ('Succ b1)

greaterEqualIndex :: forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> PeanoNatType b Source #

samePeanoGreaterEqual :: forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a Source #

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

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

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

addZeroPeanoNatTypeEqual :: forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a Source #

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

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

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

data Greater (a :: PeanoNat) (b :: PeanoNat) where Source #

Constructors

MkGreater :: forall (a1 :: PeanoNat) (b :: PeanoNat). GreaterEqual a1 b -> Greater ('Succ a1) 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 :: forall (a :: PeanoNat) (b :: PeanoNat). Greater a b -> PeanoNatType b Source #

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