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


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

module Data.TypeNat.Nat

-- | Natural numbers
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, StrongLTE m l) => Proxy l -> (forall k. LTE (S k) l => 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

-- | A constrint which includes LTE k m for every k &lt;= m.
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 GHC.Classes.Eq Data.TypeNat.Nat.Nat
instance GHC.Classes.Ord Data.TypeNat.Nat.Nat
instance Data.TypeNat.Nat.IsNat 'Data.TypeNat.Nat.Z
instance Data.TypeNat.Nat.IsNat n => Data.TypeNat.Nat.IsNat ('Data.TypeNat.Nat.S n)
instance Data.TypeNat.Nat.LTE n n
instance Data.TypeNat.Nat.LTE n m => Data.TypeNat.Nat.LTE n ('Data.TypeNat.Nat.S m)

module Data.TypeNat.Vect

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

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

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

-- | Drop the length index from a Vect, giving a typical list.
vectToList :: Vect n a -> [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 n a)

-- | Show a Vect.
showVect :: Show a => Vect l a -> String
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.TypeNat.Vect.Vect n a)
instance GHC.Show.Show a => GHC.Show.Show (Data.TypeNat.Vect.Vect n a)
instance GHC.Base.Functor (Data.TypeNat.Vect.Vect n)
instance Data.Foldable.Foldable (Data.TypeNat.Vect.Vect n)
instance Data.Traversable.Traversable (Data.TypeNat.Vect.Vect n)

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 :: Fin n -> Vect n a -> a

-- | Safely update a Vect.
safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a