Safe Haskell	Safe
Language	Haskell98

Data.Witness.Nat

Documentation

data NatType (t :: Nat) where #

Constructors

ZeroType :: NatType Zero
SuccType :: NatType t -> NatType (Succ t)

Instances

TestEquality NatType #
Instance details Defined in Data.Witness.Nat Methods testEquality :: NatType a -> NatType b -> Maybe (a :~: b) #
Representative NatType #
Instance details Defined in Data.Witness.Nat Methods getRepWitness :: NatType a -> Dict (Is NatType a) #
Eq1 NatType #
Instance details Defined in Data.Witness.Nat Methods equals1 :: NatType a -> NatType a -> Bool #
Is NatType Zero #
Instance details Defined in Data.Witness.Nat Methods representative :: NatType Zero #
Is NatType n => Is NatType (Succ n :: Nat) #
Instance details Defined in Data.Witness.Nat Methods representative :: NatType (Succ n) #