Safe Haskell  None 

Language  Haskell2010 
Synopsis
 data Nat
 class IsNat (n :: Nat) where
 natRecursion :: (forall m. b > a m > a (S m)) > (b > a Z) > (b > b) > b > a n
 class LTE (n :: Nat) (m :: Nat) where
 lteInduction :: StrongLTE m l => Proxy l > (forall k. LTE (S k) l => d k > d (S k)) > d n > d m
 lteRecursion :: (forall k. LTE n k => d (S k) > d k) > d m > d n
 type family StrongLTE (n :: Nat) (m :: Nat) :: Constraint where ...
 type Zero = Z
 type One = S Z
 type Two = S One
 type Three = S Two
 type Four = S Three
 type Five = S Four
 type Six = S Five
 type Seven = S Six
 type Eight = S Seven
 type Nine = S Eight
 type Ten = S Nine
Documentation
class IsNat (n :: Nat) where Source #
Proof that a given type is a Nat. With this fact, you can do typedirected computation.
natRecursion :: (forall m. b > a m > a (S m)) > (b > a Z) > (b > b) > b > a n Source #
class LTE (n :: Nat) (m :: Nat) where Source #
Nat n
is less than or equal to nat m
.
Comes with functions to do typedirected computation for Natindexed
datatypes.
:: 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

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