fast-nats-0.1.0.1: Natural Numbers with no overhead

Copyright (c) Kyle McKean, 2016 MIT mckean.kylej@gmail.com experimental Portable None 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) # Methodscompare :: 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) # MethodsshowsPrec :: 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.

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.