witness-0.4: values that witness types

Safe HaskellSafe
LanguageHaskell98

Data.Nat

Synopsis

Documentation

data Nat #

Constructors

Zero 
Succ Nat 

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 #

addNat :: Nat -> Nat -> Nat #

subtractFromNat :: Nat -> Nat -> Maybe Nat #

subtractFromNat a b = b - a