TypeNat-0.4.0.0: Some Nat-indexed types for GHC

Safe HaskellNone
LanguageHaskell2010

Data.TypeNat.Nat

Synopsis

Documentation

data Nat Source

Constructors

Z 
S Nat 

Instances

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 Source

Arguments

:: StrongLTE m l 
=> Proxy l 
-> (forall k. LTE (S k) l => d k -> d (S k))

The parameter l is fixed by any call to lteInduction, but due to the StrongLTE m l constraint, we have LTE j l for every j <= m. This allows us to implement the nontrivial case in the LTE p q => LTE p (S q) instance, where we need to use this function to get x :: d p and then again to get f x :: d (S p). So long as p and S p are both less or equal to l, this can be done.

-> d n 
-> d m 

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 family StrongLTE n m :: Constraint Source

A constrint which includes LTE k m for every k <= m.

Equations

StrongLTE Z m = LTE Z m 
StrongLTE (S n) m = (LTE (S n) m, StrongLTE n 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