TypeNat-0.2.0.0: Some Nat-indexed types for GHC

Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.TypeNat.Nat

Synopsis

Documentation

data Nat Source

Constructors

Z 
S Nat 

class IsNat n where Source

Proof that a given type is a Nat. With this fact, you can do type-directed computation.

Methods

natRecursion :: (forall m. b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n Source

Instances

IsNat Z 
IsNat n => IsNat (S n) 

class LTE n m where Source

Nat n is less than or equal to nat m. Comes with functions to do type-directed computation for Nat-indexed datatypes.

Methods

lteInduction :: (forall k. LTE (S k) m => d k -> d (S k)) -> d n -> d m Source

lteRecursion :: (forall k. LTE n k => d (S k) -> d k) -> d m -> d n Source

Instances

LTE n n 
LTE n m => LTE n (S m) 

type Zero = Z Source

type One = S Z Source

type Two = S One Source

type Three = S Two Source

type Five = S Four Source

type Six = S Five Source

type Seven = S Six Source

type Ten = S Nine Source