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


-- | Collection of widely reimplemented type families
--   
--   Collection of widely reimplemented type families
@package type-fun
@version 0.0.1

module TypeFun.Data.Peano
data N
Z :: N
S :: N -> N
instance GHC.Generics.Constructor TypeFun.Data.Peano.C1_1N
instance GHC.Generics.Constructor TypeFun.Data.Peano.C1_0N
instance GHC.Generics.Datatype TypeFun.Data.Peano.D1N
instance GHC.Generics.Generic TypeFun.Data.Peano.N
instance GHC.Show.Show TypeFun.Data.Peano.N
instance GHC.Read.Read TypeFun.Data.Peano.N
instance GHC.Classes.Ord TypeFun.Data.Peano.N
instance GHC.Classes.Eq TypeFun.Data.Peano.N

module TypeFun.Data.Maybe

-- | Like <tt>catMaybes</tt> for type lists

module TypeFun.Data.Eq


-- | Collection of type families on type lists. This module differs from
--   <b>Data.Singletons.Prelude.List</b> because works with <b>[*]</b> and
--   relies on GHC's type equality (~). The rest of required operations
--   like <tt>Reverse</tt> or '(:++:)' you could find in singletons
module TypeFun.Data.List

-- | Remove first argument type from anywhere in a list.

-- | Remove index from the list
type IndexOf a s = FromJust (IndexOfMay a s)
type IndexOfMay a s = IndexOfMay' Z a s
type Index idx s = FromJust (IndexMay idx s)

-- | Generates unresolvable constraint if fists element is not contained
--   inside of second
type Elem a s = NothingToConstr (IndexOfMay a s) (ElementNotFoundInList a s)

-- | Reverse of <a>Elem</a>
type NotElem a s = JustToConstr (IndexOfMay a s) (ElementIsInList a s)

-- | Count elements in a list

-- | Constanints that first argument is a sublist of second. Reduces to
--   <b>(Elem a1 b, Elem a2 b, Elem a3 b, ...)</b>
type IsPrefixOf a b = (If (IsPrefixOfBool a b) (() :: Constraint) (ListIsNotPrefixOf a b), SubList a b)
type IsNotPrefixOf a b = If (IsPrefixOfBool a b) (ListIsPrefixOf a b) (() :: Constraint)

-- | First argument is prefix of second

-- | Appends elements from first list to second if they are not presented
--   in.

-- | Append element to list if element is not already presented in

-- | Calculates intersection between two lists. Order of elements is taken
--   from first list
type Intersect a b = Indices (CatMaybes (IndicesOfMay a b)) b

-- | Checks that element <tt>a</tt> occurs in a list just once
type ElementIsUniq a s = If (Equal (S Z) (Count a s)) (() :: Constraint) (ElementIsNotUniqInList a s)

-- | Checks that all elements in list are unique
type UniqElements a = UniqElements' a a

module TypeFun.Constraint

-- | Apply constraint for each element of list