Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

- 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.

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.

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