-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Some Nat-indexed types for GHC
--   
@package TypeNat
@version 0.2.1.0

module Data.TypeNat.Nat
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Proof that a given type is a Nat. With this fact, you can do
--   type-directed computation.
class IsNat (n :: Nat)
natRecursion :: IsNat n => (forall m. b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n

-- | Nat <tt>n</tt> is less than or equal to nat <tt>m</tt>. Comes with
--   functions to do type-directed computation for Nat-indexed datatypes.
class LTE (n :: Nat) (m :: Nat)
lteInduction :: LTE n m => (forall k. LTE (S k) m => d k -> d (S k)) -> d n -> d m
lteRecursion :: LTE n m => (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
instance [incoherent] LTE n m => LTE n ('S m)
instance [incoherent] LTE n n
instance [incoherent] IsNat n => IsNat ('S n)
instance [incoherent] IsNat 'Z

module Data.TypeNat.Vect

-- | Nat-indexed list, where the nat determines the length.
data Vect :: * -> Nat -> *
VNil :: Vect a Z
VCons :: a -> Vect a n -> Vect a (S n)

-- | A kind of fmap for Vect.
vectMap :: (a -> b) -> Vect a n -> Vect b n

-- | VCons to the end of a Vect.
vectSnoc :: a -> Vect a n -> Vect a (S n)

-- | Drop the length index from a Vect, giving a typical list.
vectToList :: Vect a n -> [a]

-- | Try to produce a Vect from a list. The nat index must be fixed
--   somehow, perhaps with the help of ScopedTypeVariables.
listToVect :: IsNat n => [a] -> Maybe (Vect a n)
showVect :: Show a => Vect a l -> String

module Data.TypeNat.Fin

-- | Finite set datatype.
data Fin :: Nat -> *
FZ :: Fin (S n)
FS :: Fin k -> Fin (S k)
ix1 :: Fin (S n)
ix2 :: Fin (S (S n))
ix3 :: Fin (S (S (S n)))
ix4 :: Fin (S (S (S (S n))))
ix5 :: Fin (S (S (S (S (S n)))))
ix6 :: Fin (S (S (S (S (S (S n))))))
ix7 :: Fin (S (S (S (S (S (S (S n)))))))
ix8 :: Fin (S (S (S (S (S (S (S (S n))))))))
ix9 :: Fin (S (S (S (S (S (S (S (S (S n)))))))))
ix10 :: Fin (S (S (S (S (S (S (S (S (S (S n))))))))))

-- | Safely index a Vect.
safeIndex :: Vect a n -> Fin n -> a