fast-nats-0.1.0.1: Natural Numbers with no overhead

Copyright	(c) Kyle McKean, 2016
License	MIT
Maintainer	mckean.kylej@gmail.com
Stability	experimental
Portability	Portable
Safe Haskell	None
Language	Haskell2010

Data.Fin

Description

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

Synopsis

Documentation

data Fin n #

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 }

Instances

Eq (Fin n) #
Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
Ord (Fin n) #
Methods compare :: Fin n -> Fin n -> Ordering # (<) :: Fin n -> Fin n -> Bool # (<=) :: Fin n -> Fin n -> Bool # (>) :: Fin n -> Fin n -> Bool # (>=) :: Fin n -> Fin n -> Bool # max :: Fin n -> Fin n -> Fin n # min :: Fin n -> Fin n -> Fin n #
Show (Fin n) #
Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #

finToInt :: Fin n -> Int #

Get the value out of a Fin. This function has a postcondition that the Int x is 0 <= x < n

natToFin :: SNat n -> SNat m -> Maybe (Fin m) #

Given a value and a bound construct a finite set.

finToNat :: IsNat n => Fin n -> SNat n #

Get the size of the finite set.

finZAbsurd :: Fin Z -> Void #

An empty finite set is uninhabited.

finZElim :: Fin Z -> a #

Construct any value from an empty finite set as it is uninhabited.

zero :: Fin (S n) #

The smallest finite set, it only contains 0.

succ :: Fin n -> Fin (S n) #

Increase the value and bound of a finite set by one.

weaken :: Fin n -> Fin (S n) #

Increase the bound of a finite set by one.

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.

weakenN :: SNat n -> Fin m -> Fin (n + m) #

Increase the bound on a finite set by n.

strengthen :: forall n. IsNat n => Fin (S n) -> Maybe (Fin n) #

Attempt to lower a bound on a finite set by one.

shift :: SNat n -> Fin m -> Fin (n + m) #

Increase the value and bound of a finite set by N.

last :: forall n. IsNat n => Fin (S n) #

Construct the largest value possible in a finite set.