Safe Haskell | None |
---|---|

Language | Haskell2010 |

- data Nat
- class IsNat n where
- class LTE n m where
- 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

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

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.