Copyright | (c) Kyle McKean, 2016 |
---|---|

License | MIT |

Maintainer | mckean.kylej@gmail.com |

Stability | experimental |

Portability | Portable |

Safe Haskell | None |

Language | Haskell2010 |

Fast finite sets, you can learn more about these types from agda and idris' standard libary.

- data Fin n
- finToInt :: Fin n -> Int
- natToFin :: SNat n -> SNat m -> Maybe (Fin m)
- finToNat :: IsNat n => Fin n -> SNat n
- finZAbsurd :: Fin Z -> Void
- finZElim :: Fin Z -> a
- zero :: Fin (S n)
- succ :: Fin n -> Fin (S n)
- weaken :: Fin n -> Fin (S n)
- weakenLTE :: LTE n m -> Fin n -> Fin m
- weakenN :: SNat n -> Fin m -> Fin (n + m)
- strengthen :: forall n. IsNat n => Fin (S n) -> Maybe (Fin n)
- shift :: SNat n -> Fin m -> Fin (n + m)
- last :: forall n. IsNat n => Fin (S n)

# Documentation

Finite Sets, this type has an upper bound n and can only contain numbers between ∀x. 0 <= x < n

Fin 1 = { 0 }

Fin 2 = { 0, 1 }

Fin 3 = { 0, 1, 2 }

finZAbsurd :: Fin Z -> Void #

An empty finite set is uninhabited.

weakenLTE :: LTE n m -> Fin n -> Fin m #

Given a proof that n is less than or equal to m weaken a finite set of bound n to bound m.