witness-0.4: values that witness types

Safe HaskellSafe
LanguageHaskell98

Data.Witness.Nat

Documentation

data NatType t where #

Constructors

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

Instances

TestEquality Nat NatType # 

Methods

testEquality :: f a -> f b -> Maybe ((NatType :~: a) b) #

Representative Nat NatType # 

Methods

getRepWitness :: rep a -> Dict (Is NatType rep a) #

Eq1 Nat NatType # 

Methods

equals1 :: p a -> p a -> Bool #

Is Nat NatType Zero # 

Methods

representative :: Zero a #

Is Nat NatType n => Is Nat NatType (Succ n) # 

Methods

representative :: Succ n a #