| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.TypeNat.Nat
- data Nat
- class IsNat n where
- natRecursion :: (forall m. b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n
- class LTE n m where
- lteInduction :: (forall k. LTE (S k) m => 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 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
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
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