witness-0.4: values that witness types

Safe HaskellSafe
LanguageHaskell98

Data.Nat

Synopsis

Documentation

data Nat Source #

Constructors

Zero 
Succ Nat 

Instances

TestEquality Nat NatType # 

Methods

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

Representative Nat NatType Source # 

Methods

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

Eq1 Nat NatType Source # 

Methods

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

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

Methods

representative :: Succ n a Source #

addNat :: Nat -> Nat -> Nat Source #

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

subtractFromNat a b = b - a

multiplyNat :: Nat -> Nat -> Nat Source #