Data.Singletons.Prelude.List

Contents

• The singleton for lists
• Basic functions
• List transformations
• Reducing lists (folds)
  • Special folds
• Building lists
  • Scans
  • Accumulating maps
  • Cyclical lists
  • Unfolding
• Sublists
  • Extracting sublists
  • Predicates
• Searching lists
  • Searching by equality
  • Searching with a predicate
• Indexing lists
• Zipping and unzipping lists
• Special lists
  • "Set" operations
  • Ordered lists
• Generalized functions
  • The "By" operations
    • User-supplied equality (replacing an Eq context)
    • User-supplied comparison (replacing an Ord context)
  • The "generic" operations
• Defunctionalization symbols

Description

Synopsis

• data family Sing (a :: k)
• type SList = (Sing :: [a] -> Type)
• type family (a :: [a]) :++ (a :: [a]) :: [a] where ...
• (%:++) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (:++$) t) t :: [a])
• type family Head (a :: [a]) :: a where ...
• sHead :: forall (t :: [a]). Sing t -> Sing (Apply HeadSym0 t :: a)
• type family Last (a :: [a]) :: a where ...
• sLast :: forall (t :: [a]). Sing t -> Sing (Apply LastSym0 t :: a)
• type family Tail (a :: [a]) :: [a] where ...
• sTail :: forall (t :: [a]). Sing t -> Sing (Apply TailSym0 t :: [a])
• type family Init (a :: [a]) :: [a] where ...
• sInit :: forall (t :: [a]). Sing t -> Sing (Apply InitSym0 t :: [a])
• type family Null (a :: [a]) :: Bool where ...
• sNull :: forall (t :: [a]). Sing t -> Sing (Apply NullSym0 t :: Bool)
• type family Length (a :: [a]) :: Nat where ...
• sLength :: forall (t :: [a]). Sing t -> Sing (Apply LengthSym0 t :: Nat)
• type family Map (a :: TyFun a b -> Type) (a :: [a]) :: [b] where ...
• sMap :: forall (t :: TyFun a b -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b])
• type family Reverse (a :: [a]) :: [a] where ...
• sReverse :: forall (t :: [a]). Sing t -> Sing (Apply ReverseSym0 t :: [a])
• type family Intersperse (a :: a) (a :: [a]) :: [a] where ...
• sIntersperse :: forall (t :: a) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply IntersperseSym0 t) t :: [a])
• type family Intercalate (a :: [a]) (a :: [[a]]) :: [a] where ...
• sIntercalate :: forall (t :: [a]) (t :: [[a]]). Sing t -> Sing t -> Sing (Apply (Apply IntercalateSym0 t) t :: [a])
• type family Transpose (a :: [[a]]) :: [[a]] where ...
• sTranspose :: forall (t :: [[a]]). Sing t -> Sing (Apply TransposeSym0 t :: [[a]])
• type family Subsequences (a :: [a]) :: [[a]] where ...
• sSubsequences :: forall (t :: [a]). Sing t -> Sing (Apply SubsequencesSym0 t :: [[a]])
• type family Permutations (a :: [a]) :: [[a]] where ...
• sPermutations :: forall (t :: [a]). Sing t -> Sing (Apply PermutationsSym0 t :: [[a]])
• type family Foldl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...
• sFoldl :: forall (t :: TyFun b (TyFun a b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t :: b)
• type family Foldl' (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...
• sFoldl' :: forall (t :: TyFun b (TyFun a b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t :: b)
• type family Foldl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...
• sFoldl1 :: forall (t :: TyFun a (TyFun a a -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t :: a)
• type family Foldl1' (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...
• sFoldl1' :: forall (t :: TyFun a (TyFun a a -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Foldl1'Sym0 t) t :: a)
• type family Foldr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...
• sFoldr :: forall (t :: TyFun a (TyFun b b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b)
• type family Foldr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...
• sFoldr1 :: forall (t :: TyFun a (TyFun a a -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t :: a)
• type family Concat (a :: [[a]]) :: [a] where ...
• sConcat :: forall (t :: [[a]]). Sing t -> Sing (Apply ConcatSym0 t :: [a])
• type family ConcatMap (a :: TyFun a [b] -> Type) (a :: [a]) :: [b] where ...
• sConcatMap :: forall (t :: TyFun a [b] -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply ConcatMapSym0 t) t :: [b])
• type family And (a :: [Bool]) :: Bool where ...
• sAnd :: forall (t :: [Bool]). Sing t -> Sing (Apply AndSym0 t :: Bool)
• type family Or (a :: [Bool]) :: Bool where ...
• sOr :: forall (t :: [Bool]). Sing t -> Sing (Apply OrSym0 t :: Bool)
• type family Any_ (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...
• sAny_ :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Any_Sym0 t) t :: Bool)
• type family All (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...
• sAll :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply AllSym0 t) t :: Bool)
• type family Sum (a :: [a]) :: a where ...
• sSum :: forall (t :: [a]). SNum a => Sing t -> Sing (Apply SumSym0 t :: a)
• type family Product (a :: [a]) :: a where ...
• sProduct :: forall (t :: [a]). SNum a => Sing t -> Sing (Apply ProductSym0 t :: a)
• type family Maximum (a :: [a]) :: a where ...
• sMaximum :: forall (t :: [a]). SOrd a => Sing t -> Sing (Apply MaximumSym0 t :: a)
• type family Minimum (a :: [a]) :: a where ...
• sMinimum :: forall (t :: [a]). SOrd a => Sing t -> Sing (Apply MinimumSym0 t :: a)
• any_ :: (a -> Bool) -> [a] -> Bool
• type family Scanl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...
• sScanl :: forall (t :: TyFun b (TyFun a b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanlSym0 t) t) t :: [b])
• type family Scanl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...
• sScanl1 :: forall (t :: TyFun a (TyFun a a -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Scanl1Sym0 t) t :: [a])
• type family Scanr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...
• sScanr :: forall (t :: TyFun a (TyFun b b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanrSym0 t) t) t :: [b])
• type family Scanr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...
• sScanr1 :: forall (t :: TyFun a (TyFun a a -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Scanr1Sym0 t) t :: [a])
• type family MapAccumL (a :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (a :: acc) (a :: [x]) :: (acc, [y]) where ...
• sMapAccumL :: forall (t :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (t :: acc) (t :: [x]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply MapAccumLSym0 t) t) t :: (acc, [y]))
• type family MapAccumR (a :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (a :: acc) (a :: [x]) :: (acc, [y]) where ...
• sMapAccumR :: forall (t :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (t :: acc) (t :: [x]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply MapAccumRSym0 t) t) t :: (acc, [y]))
• type family Replicate (a :: Nat) (a :: a) :: [a] where ...
• sReplicate :: forall (t :: Nat) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ReplicateSym0 t) t :: [a])
• type family Unfoldr (a :: TyFun b (Maybe (a, b)) -> Type) (a :: b) :: [a] where ...
• sUnfoldr :: forall (t :: TyFun b (Maybe (a, b)) -> Type) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply UnfoldrSym0 t) t :: [a])
• type family Take (a :: Nat) (a :: [a]) :: [a] where ...
• sTake :: forall (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply TakeSym0 t) t :: [a])
• type family Drop (a :: Nat) (a :: [a]) :: [a] where ...
• sDrop :: forall (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply DropSym0 t) t :: [a])
• type family SplitAt (a :: Nat) (a :: [a]) :: ([a], [a]) where ...
• sSplitAt :: forall (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply SplitAtSym0 t) t :: ([a], [a]))
• type family TakeWhile (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...
• sTakeWhile :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply TakeWhileSym0 t) t :: [a])
• type family DropWhile (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...
• sDropWhile :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply DropWhileSym0 t) t :: [a])
• type family DropWhileEnd (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...
• sDropWhileEnd :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply DropWhileEndSym0 t) t :: [a])
• type family Span (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...
• sSpan :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply SpanSym0 t) t :: ([a], [a]))
• type family Break (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...
• sBreak :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply BreakSym0 t) t :: ([a], [a]))
• type family Group (a :: [a]) :: [[a]] where ...
• sGroup :: forall (t :: [a]). SEq a => Sing t -> Sing (Apply GroupSym0 t :: [[a]])
• type family Inits (a :: [a]) :: [[a]] where ...
• sInits :: forall (t :: [a]). Sing t -> Sing (Apply InitsSym0 t :: [[a]])
• type family Tails (a :: [a]) :: [[a]] where ...
• sTails :: forall (t :: [a]). Sing t -> Sing (Apply TailsSym0 t :: [[a]])
• type family IsPrefixOf (a :: [a]) (a :: [a]) :: Bool where ...
• sIsPrefixOf :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply IsPrefixOfSym0 t) t :: Bool)
• type family IsSuffixOf (a :: [a]) (a :: [a]) :: Bool where ...
• sIsSuffixOf :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply IsSuffixOfSym0 t) t :: Bool)
• type family IsInfixOf (a :: [a]) (a :: [a]) :: Bool where ...
• sIsInfixOf :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply IsInfixOfSym0 t) t :: Bool)
• type family Elem (a :: a) (a :: [a]) :: Bool where ...
• sElem :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t :: Bool)
• type family NotElem (a :: a) (a :: [a]) :: Bool where ...
• sNotElem :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply NotElemSym0 t) t :: Bool)
• type family Lookup (a :: a) (a :: [(a, b)]) :: Maybe b where ...
• sLookup :: forall (t :: a) (t :: [(a, b)]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: Maybe b)
• type family Find (a :: TyFun a Bool -> Type) (a :: [a]) :: Maybe a where ...
• sFind :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FindSym0 t) t :: Maybe a)
• type family Filter (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...
• sFilter :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FilterSym0 t) t :: [a])
• type family Partition (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...
• sPartition :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply PartitionSym0 t) t :: ([a], [a]))
• type family (a :: [a]) :!! (a :: Nat) :: a where ...
• (%:!!) :: forall (t :: [a]) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (:!!$) t) t :: a)
• type family ElemIndex (a :: a) (a :: [a]) :: Maybe Nat where ...
• sElemIndex :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemIndexSym0 t) t :: Maybe Nat)
• type family ElemIndices (a :: a) (a :: [a]) :: [Nat] where ...
• sElemIndices :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemIndicesSym0 t) t :: [Nat])
• type family FindIndex (a :: TyFun a Bool -> Type) (a :: [a]) :: Maybe Nat where ...
• sFindIndex :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FindIndexSym0 t) t :: Maybe Nat)
• type family FindIndices (a :: TyFun a Bool -> Type) (a :: [a]) :: [Nat] where ...
• sFindIndices :: forall (t :: TyFun a Bool -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FindIndicesSym0 t) t :: [Nat])
• type family Zip (a :: [a]) (a :: [b]) :: [(a, b)] where ...
• sZip :: forall (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply ZipSym0 t) t :: [(a, b)])
• type family Zip3 (a :: [a]) (a :: [b]) (a :: [c]) :: [(a, b, c)] where ...
• sZip3 :: forall (t :: [a]) (t :: [b]) (t :: [c]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Zip3Sym0 t) t) t :: [(a, b, c)])
• type family ZipWith (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: [a]) (a :: [b]) :: [c] where ...
• sZipWith :: forall (t :: TyFun a (TyFun b c -> Type) -> Type) (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c])
• type family ZipWith3 (a :: TyFun a (TyFun b (TyFun c d -> Type) -> Type) -> Type) (a :: [a]) (a :: [b]) (a :: [c]) :: [d] where ...
• sZipWith3 :: forall (t :: TyFun a (TyFun b (TyFun c d -> Type) -> Type) -> Type) (t :: [a]) (t :: [b]) (t :: [c]). Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply ZipWith3Sym0 t) t) t) t :: [d])
• type family Unzip (a :: [(a, b)]) :: ([a], [b]) where ...
• sUnzip :: forall (t :: [(a, b)]). Sing t -> Sing (Apply UnzipSym0 t :: ([a], [b]))
• type family Unzip3 (a :: [(a, b, c)]) :: ([a], [b], [c]) where ...
• sUnzip3 :: forall (t :: [(a, b, c)]). Sing t -> Sing (Apply Unzip3Sym0 t :: ([a], [b], [c]))
• type family Unzip4 (a :: [(a, b, c, d)]) :: ([a], [b], [c], [d]) where ...
• sUnzip4 :: forall (t :: [(a, b, c, d)]). Sing t -> Sing (Apply Unzip4Sym0 t :: ([a], [b], [c], [d]))
• type family Unzip5 (a :: [(a, b, c, d, e)]) :: ([a], [b], [c], [d], [e]) where ...
• sUnzip5 :: forall (t :: [(a, b, c, d, e)]). Sing t -> Sing (Apply Unzip5Sym0 t :: ([a], [b], [c], [d], [e]))
• type family Unzip6 (a :: [(a, b, c, d, e, f)]) :: ([a], [b], [c], [d], [e], [f]) where ...
• sUnzip6 :: forall (t :: [(a, b, c, d, e, f)]). Sing t -> Sing (Apply Unzip6Sym0 t :: ([a], [b], [c], [d], [e], [f]))
• type family Unzip7 (a :: [(a, b, c, d, e, f, g)]) :: ([a], [b], [c], [d], [e], [f], [g]) where ...
• sUnzip7 :: forall (t :: [(a, b, c, d, e, f, g)]). Sing t -> Sing (Apply Unzip7Sym0 t :: ([a], [b], [c], [d], [e], [f], [g]))
• type family Nub (a :: [a]) :: [a] where ...
• sNub :: forall (t :: [a]). SEq a => Sing t -> Sing (Apply NubSym0 t :: [a])
• type family Delete (a :: a) (a :: [a]) :: [a] where ...
• sDelete :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply DeleteSym0 t) t :: [a])
• type family (a :: [a]) :\\ (a :: [a]) :: [a] where ...
• (%:\\) :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply (:\\$) t) t :: [a])
• type family Union (a :: [a]) (a :: [a]) :: [a] where ...
• sUnion :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply UnionSym0 t) t :: [a])
• type family Intersect (a :: [a]) (a :: [a]) :: [a] where ...
• sIntersect :: forall (t :: [a]) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply IntersectSym0 t) t :: [a])
• type family Insert (a :: a) (a :: [a]) :: [a] where ...
• sInsert :: forall (t :: a) (t :: [a]). SOrd a => Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [a])
• type family Sort (a :: [a]) :: [a] where ...
• sSort :: forall (t :: [a]). SOrd a => Sing t -> Sing (Apply SortSym0 t :: [a])
• type family NubBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) :: [a] where ...
• sNubBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply NubBySym0 t) t :: [a])
• type family DeleteBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: a) (a :: [a]) :: [a] where ...
• sDeleteBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: a) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply DeleteBySym0 t) t) t :: [a])
• type family DeleteFirstsBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...
• sDeleteFirstsBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply DeleteFirstsBySym0 t) t) t :: [a])
• type family UnionBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...
• sUnionBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply UnionBySym0 t) t) t :: [a])
• type family IntersectBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...
• sIntersectBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply IntersectBySym0 t) t) t :: [a])
• type family GroupBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) :: [[a]] where ...
• sGroupBy :: forall (t :: TyFun a (TyFun a Bool -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply GroupBySym0 t) t :: [[a]])
• type family SortBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: [a] where ...
• sSortBy :: forall (t :: TyFun a (TyFun a Ordering -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply SortBySym0 t) t :: [a])
• type family InsertBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: a) (a :: [a]) :: [a] where ...
• sInsertBy :: forall (t :: TyFun a (TyFun a Ordering -> Type) -> Type) (t :: a) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply InsertBySym0 t) t) t :: [a])
• type family MaximumBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: a where ...
• sMaximumBy :: forall (t :: TyFun a (TyFun a Ordering -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MaximumBySym0 t) t :: a)
• type family MinimumBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: a where ...
• sMinimumBy :: forall (t :: TyFun a (TyFun a Ordering -> Type) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MinimumBySym0 t) t :: a)
• type family GenericLength (a :: [a]) :: i where ...
• sGenericLength :: forall (t :: [a]). SNum i => Sing t -> Sing (Apply GenericLengthSym0 t :: i)
• type NilSym0 = '[]
• data (:$) (l :: TyFun a3530822107858468865 (TyFun [a3530822107858468865] [a3530822107858468865] -> Type))
• data (l :: a3530822107858468865) :$$ (l :: TyFun [a3530822107858468865] [a3530822107858468865])
• type (:$$$) (t :: a3530822107858468865) (t :: [a3530822107858468865]) = (:) t t
• type (:++$$$) (t :: [a6989586621679281045]) (t :: [a6989586621679281045]) = (:++) t t
• data (l :: [a6989586621679281045]) :++$$ (l :: TyFun [a6989586621679281045] [a6989586621679281045])
• data (:++$) (l :: TyFun [a6989586621679281045] (TyFun [a6989586621679281045] [a6989586621679281045] -> Type))
• data HeadSym0 (l :: TyFun [a6989586621679458196] a6989586621679458196)
• type HeadSym1 (t :: [a6989586621679458196]) = Head t
• data LastSym0 (l :: TyFun [a6989586621679458195] a6989586621679458195)
• type LastSym1 (t :: [a6989586621679458195]) = Last t
• data TailSym0 (l :: TyFun [a6989586621679458194] [a6989586621679458194])
• type TailSym1 (t :: [a6989586621679458194]) = Tail t
• data InitSym0 (l :: TyFun [a6989586621679458193] [a6989586621679458193])
• type InitSym1 (t :: [a6989586621679458193]) = Init t
• data NullSym0 (l :: TyFun [a6989586621679458192] Bool)
• type NullSym1 (t :: [a6989586621679458192]) = Null t
• data LengthSym0 (l :: TyFun [a6989586621679458079] Nat)
• type LengthSym1 (t :: [a6989586621679458079]) = Length t
• data MapSym0 (l :: TyFun (TyFun a6989586621679281046 b6989586621679281047 -> Type) (TyFun [a6989586621679281046] [b6989586621679281047] -> Type))
• data MapSym1 (l :: TyFun a6989586621679281046 b6989586621679281047 -> Type) (l :: TyFun [a6989586621679281046] [b6989586621679281047])
• type MapSym2 (t :: TyFun a6989586621679281046 b6989586621679281047 -> Type) (t :: [a6989586621679281046]) = Map t t
• data ReverseSym0 (l :: TyFun [a6989586621679458191] [a6989586621679458191])
• type ReverseSym1 (t :: [a6989586621679458191]) = Reverse t
• data IntersperseSym0 (l :: TyFun a6989586621679458190 (TyFun [a6989586621679458190] [a6989586621679458190] -> Type))
• data IntersperseSym1 (l :: a6989586621679458190) (l :: TyFun [a6989586621679458190] [a6989586621679458190])
• type IntersperseSym2 (t :: a6989586621679458190) (t :: [a6989586621679458190]) = Intersperse t t
• data IntercalateSym0 (l :: TyFun [a6989586621679458189] (TyFun [[a6989586621679458189]] [a6989586621679458189] -> Type))
• data IntercalateSym1 (l :: [a6989586621679458189]) (l :: TyFun [[a6989586621679458189]] [a6989586621679458189])
• type IntercalateSym2 (t :: [a6989586621679458189]) (t :: [[a6989586621679458189]]) = Intercalate t t
• data TransposeSym0 (l :: TyFun [[a6989586621679458077]] [[a6989586621679458077]])
• type TransposeSym1 (t :: [[a6989586621679458077]]) = Transpose t
• data SubsequencesSym0 (l :: TyFun [a6989586621679458188] [[a6989586621679458188]])
• type SubsequencesSym1 (t :: [a6989586621679458188]) = Subsequences t
• data PermutationsSym0 (l :: TyFun [a6989586621679458185] [[a6989586621679458185]])
• type PermutationsSym1 (t :: [a6989586621679458185]) = Permutations t
• data FoldlSym0 (l :: TyFun (TyFun b6989586621679242246 (TyFun a6989586621679242245 b6989586621679242246 -> Type) -> Type) (TyFun b6989586621679242246 (TyFun [a6989586621679242245] b6989586621679242246 -> Type) -> Type))
• data FoldlSym1 (l :: TyFun b6989586621679242246 (TyFun a6989586621679242245 b6989586621679242246 -> Type) -> Type) (l :: TyFun b6989586621679242246 (TyFun [a6989586621679242245] b6989586621679242246 -> Type))
• data FoldlSym2 (l :: TyFun b6989586621679242246 (TyFun a6989586621679242245 b6989586621679242246 -> Type) -> Type) (l :: b6989586621679242246) (l :: TyFun [a6989586621679242245] b6989586621679242246)
• type FoldlSym3 (t :: TyFun b6989586621679242246 (TyFun a6989586621679242245 b6989586621679242246 -> Type) -> Type) (t :: b6989586621679242246) (t :: [a6989586621679242245]) = Foldl t t t
• data Foldl'Sym0 (l :: TyFun (TyFun b6989586621679458184 (TyFun a6989586621679458183 b6989586621679458184 -> Type) -> Type) (TyFun b6989586621679458184 (TyFun [a6989586621679458183] b6989586621679458184 -> Type) -> Type))
• data Foldl'Sym1 (l :: TyFun b6989586621679458184 (TyFun a6989586621679458183 b6989586621679458184 -> Type) -> Type) (l :: TyFun b6989586621679458184 (TyFun [a6989586621679458183] b6989586621679458184 -> Type))
• data Foldl'Sym2 (l :: TyFun b6989586621679458184 (TyFun a6989586621679458183 b6989586621679458184 -> Type) -> Type) (l :: b6989586621679458184) (l :: TyFun [a6989586621679458183] b6989586621679458184)
• type Foldl'Sym3 (t :: TyFun b6989586621679458184 (TyFun a6989586621679458183 b6989586621679458184 -> Type) -> Type) (t :: b6989586621679458184) (t :: [a6989586621679458183]) = Foldl' t t t
• data Foldl1Sym0 (l :: TyFun (TyFun a6989586621679458182 (TyFun a6989586621679458182 a6989586621679458182 -> Type) -> Type) (TyFun [a6989586621679458182] a6989586621679458182 -> Type))
• data Foldl1Sym1 (l :: TyFun a6989586621679458182 (TyFun a6989586621679458182 a6989586621679458182 -> Type) -> Type) (l :: TyFun [a6989586621679458182] a6989586621679458182)
• type Foldl1Sym2 (t :: TyFun a6989586621679458182 (TyFun a6989586621679458182 a6989586621679458182 -> Type) -> Type) (t :: [a6989586621679458182]) = Foldl1 t t
• data Foldl1'Sym0 (l :: TyFun (TyFun a6989586621679458181 (TyFun a6989586621679458181 a6989586621679458181 -> Type) -> Type) (TyFun [a6989586621679458181] a6989586621679458181 -> Type))
• data Foldl1'Sym1 (l :: TyFun a6989586621679458181 (TyFun a6989586621679458181 a6989586621679458181 -> Type) -> Type) (l :: TyFun [a6989586621679458181] a6989586621679458181)
• type Foldl1'Sym2 (t :: TyFun a6989586621679458181 (TyFun a6989586621679458181 a6989586621679458181 -> Type) -> Type) (t :: [a6989586621679458181]) = Foldl1' t t
• data FoldrSym0 (l :: TyFun (TyFun a6989586621679281048 (TyFun b6989586621679281049 b6989586621679281049 -> Type) -> Type) (TyFun b6989586621679281049 (TyFun [a6989586621679281048] b6989586621679281049 -> Type) -> Type))
• data FoldrSym1 (l :: TyFun a6989586621679281048 (TyFun b6989586621679281049 b6989586621679281049 -> Type) -> Type) (l :: TyFun b6989586621679281049 (TyFun [a6989586621679281048] b6989586621679281049 -> Type))
• data FoldrSym2 (l :: TyFun a6989586621679281048 (TyFun b6989586621679281049 b6989586621679281049 -> Type) -> Type) (l :: b6989586621679281049) (l :: TyFun [a6989586621679281048] b6989586621679281049)
• type FoldrSym3 (t :: TyFun a6989586621679281048 (TyFun b6989586621679281049 b6989586621679281049 -> Type) -> Type) (t :: b6989586621679281049) (t :: [a6989586621679281048]) = Foldr t t t
• data Foldr1Sym0 (l :: TyFun (TyFun a6989586621679458180 (TyFun a6989586621679458180 a6989586621679458180 -> Type) -> Type) (TyFun [a6989586621679458180] a6989586621679458180 -> Type))
• data Foldr1Sym1 (l :: TyFun a6989586621679458180 (TyFun a6989586621679458180 a6989586621679458180 -> Type) -> Type) (l :: TyFun [a6989586621679458180] a6989586621679458180)
• type Foldr1Sym2 (t :: TyFun a6989586621679458180 (TyFun a6989586621679458180 a6989586621679458180 -> Type) -> Type) (t :: [a6989586621679458180]) = Foldr1 t t
• data ConcatSym0 (l :: TyFun [[a6989586621679458179]] [a6989586621679458179])
• type ConcatSym1 (t :: [[a6989586621679458179]]) = Concat t
• data ConcatMapSym0 (l :: TyFun (TyFun a6989586621679458177 [b6989586621679458178] -> Type) (TyFun [a6989586621679458177] [b6989586621679458178] -> Type))
• data ConcatMapSym1 (l :: TyFun a6989586621679458177 [b6989586621679458178] -> Type) (l :: TyFun [a6989586621679458177] [b6989586621679458178])
• type ConcatMapSym2 (t :: TyFun a6989586621679458177 [b6989586621679458178] -> Type) (t :: [a6989586621679458177]) = ConcatMap t t
• data AndSym0 (l :: TyFun [Bool] Bool)
• type AndSym1 (t :: [Bool]) = And t
• data OrSym0 (l :: TyFun [Bool] Bool)
• type OrSym1 (t :: [Bool]) = Or t
• data Any_Sym0 (l :: TyFun (TyFun a6989586621679447960 Bool -> Type) (TyFun [a6989586621679447960] Bool -> Type))
• data Any_Sym1 (l :: TyFun a6989586621679447960 Bool -> Type) (l :: TyFun [a6989586621679447960] Bool)
• type Any_Sym2 (t :: TyFun a6989586621679447960 Bool -> Type) (t :: [a6989586621679447960]) = Any_ t t
• data AllSym0 (l :: TyFun (TyFun a6989586621679458176 Bool -> Type) (TyFun [a6989586621679458176] Bool -> Type))
• data AllSym1 (l :: TyFun a6989586621679458176 Bool -> Type) (l :: TyFun [a6989586621679458176] Bool)
• type AllSym2 (t :: TyFun a6989586621679458176 Bool -> Type) (t :: [a6989586621679458176]) = All t t
• data SumSym0 (l :: TyFun [a6989586621679458081] a6989586621679458081)
• type SumSym1 (t :: [a6989586621679458081]) = Sum t
• data ProductSym0 (l :: TyFun [a6989586621679458080] a6989586621679458080)
• type ProductSym1 (t :: [a6989586621679458080]) = Product t
• data MaximumSym0 (l :: TyFun [a6989586621679458090] a6989586621679458090)
• type MaximumSym1 (t :: [a6989586621679458090]) = Maximum t
• data MinimumSym0 (l :: TyFun [a6989586621679458089] a6989586621679458089)
• type MinimumSym1 (t :: [a6989586621679458089]) = Minimum t
• data ScanlSym0 (l :: TyFun (TyFun b6989586621679458174 (TyFun a6989586621679458175 b6989586621679458174 -> Type) -> Type) (TyFun b6989586621679458174 (TyFun [a6989586621679458175] [b6989586621679458174] -> Type) -> Type))
• data ScanlSym1 (l :: TyFun b6989586621679458174 (TyFun a6989586621679458175 b6989586621679458174 -> Type) -> Type) (l :: TyFun b6989586621679458174 (TyFun [a6989586621679458175] [b6989586621679458174] -> Type))
• data ScanlSym2 (l :: TyFun b6989586621679458174 (TyFun a6989586621679458175 b6989586621679458174 -> Type) -> Type) (l :: b6989586621679458174) (l :: TyFun [a6989586621679458175] [b6989586621679458174])
• type ScanlSym3 (t :: TyFun b6989586621679458174 (TyFun a6989586621679458175 b6989586621679458174 -> Type) -> Type) (t :: b6989586621679458174) (t :: [a6989586621679458175]) = Scanl t t t
• data Scanl1Sym0 (l :: TyFun (TyFun a6989586621679458173 (TyFun a6989586621679458173 a6989586621679458173 -> Type) -> Type) (TyFun [a6989586621679458173] [a6989586621679458173] -> Type))
• data Scanl1Sym1 (l :: TyFun a6989586621679458173 (TyFun a6989586621679458173 a6989586621679458173 -> Type) -> Type) (l :: TyFun [a6989586621679458173] [a6989586621679458173])
• type Scanl1Sym2 (t :: TyFun a6989586621679458173 (TyFun a6989586621679458173 a6989586621679458173 -> Type) -> Type) (t :: [a6989586621679458173]) = Scanl1 t t
• data ScanrSym0 (l :: TyFun (TyFun a6989586621679458171 (TyFun b6989586621679458172 b6989586621679458172 -> Type) -> Type) (TyFun b6989586621679458172 (TyFun [a6989586621679458171] [b6989586621679458172] -> Type) -> Type))
• data ScanrSym1 (l :: TyFun a6989586621679458171 (TyFun b6989586621679458172 b6989586621679458172 -> Type) -> Type) (l :: TyFun b6989586621679458172 (TyFun [a6989586621679458171] [b6989586621679458172] -> Type))
• data ScanrSym2 (l :: TyFun a6989586621679458171 (TyFun b6989586621679458172 b6989586621679458172 -> Type) -> Type) (l :: b6989586621679458172) (l :: TyFun [a6989586621679458171] [b6989586621679458172])
• type ScanrSym3 (t :: TyFun a6989586621679458171 (TyFun b6989586621679458172 b6989586621679458172 -> Type) -> Type) (t :: b6989586621679458172) (t :: [a6989586621679458171]) = Scanr t t t
• data Scanr1Sym0 (l :: TyFun (TyFun a6989586621679458170 (TyFun a6989586621679458170 a6989586621679458170 -> Type) -> Type) (TyFun [a6989586621679458170] [a6989586621679458170] -> Type))
• data Scanr1Sym1 (l :: TyFun a6989586621679458170 (TyFun a6989586621679458170 a6989586621679458170 -> Type) -> Type) (l :: TyFun [a6989586621679458170] [a6989586621679458170])
• type Scanr1Sym2 (t :: TyFun a6989586621679458170 (TyFun a6989586621679458170 a6989586621679458170 -> Type) -> Type) (t :: [a6989586621679458170]) = Scanr1 t t
• data MapAccumLSym0 (l :: TyFun (TyFun acc6989586621679458167 (TyFun x6989586621679458168 (acc6989586621679458167, y6989586621679458169) -> Type) -> Type) (TyFun acc6989586621679458167 (TyFun [x6989586621679458168] (acc6989586621679458167, [y6989586621679458169]) -> Type) -> Type))
• data MapAccumLSym1 (l :: TyFun acc6989586621679458167 (TyFun x6989586621679458168 (acc6989586621679458167, y6989586621679458169) -> Type) -> Type) (l :: TyFun acc6989586621679458167 (TyFun [x6989586621679458168] (acc6989586621679458167, [y6989586621679458169]) -> Type))
• data MapAccumLSym2 (l :: TyFun acc6989586621679458167 (TyFun x6989586621679458168 (acc6989586621679458167, y6989586621679458169) -> Type) -> Type) (l :: acc6989586621679458167) (l :: TyFun [x6989586621679458168] (acc6989586621679458167, [y6989586621679458169]))
• type MapAccumLSym3 (t :: TyFun acc6989586621679458167 (TyFun x6989586621679458168 (acc6989586621679458167, y6989586621679458169) -> Type) -> Type) (t :: acc6989586621679458167) (t :: [x6989586621679458168]) = MapAccumL t t t
• data MapAccumRSym0 (l :: TyFun (TyFun acc6989586621679458164 (TyFun x6989586621679458165 (acc6989586621679458164, y6989586621679458166) -> Type) -> Type) (TyFun acc6989586621679458164 (TyFun [x6989586621679458165] (acc6989586621679458164, [y6989586621679458166]) -> Type) -> Type))
• data MapAccumRSym1 (l :: TyFun acc6989586621679458164 (TyFun x6989586621679458165 (acc6989586621679458164, y6989586621679458166) -> Type) -> Type) (l :: TyFun acc6989586621679458164 (TyFun [x6989586621679458165] (acc6989586621679458164, [y6989586621679458166]) -> Type))
• data MapAccumRSym2 (l :: TyFun acc6989586621679458164 (TyFun x6989586621679458165 (acc6989586621679458164, y6989586621679458166) -> Type) -> Type) (l :: acc6989586621679458164) (l :: TyFun [x6989586621679458165] (acc6989586621679458164, [y6989586621679458166]))
• type MapAccumRSym3 (t :: TyFun acc6989586621679458164 (TyFun x6989586621679458165 (acc6989586621679458164, y6989586621679458166) -> Type) -> Type) (t :: acc6989586621679458164) (t :: [x6989586621679458165]) = MapAccumR t t t
• data ReplicateSym0 (l :: TyFun Nat (TyFun a6989586621679458078 [a6989586621679458078] -> Type))
• data ReplicateSym1 (l :: Nat) (l :: TyFun a6989586621679458078 [a6989586621679458078])
• type ReplicateSym2 (t :: Nat) (t :: a6989586621679458078) = Replicate t t
• data UnfoldrSym0 (l :: TyFun (TyFun b6989586621679458162 (Maybe (a6989586621679458163, b6989586621679458162)) -> Type) (TyFun b6989586621679458162 [a6989586621679458163] -> Type))
• data UnfoldrSym1 (l :: TyFun b6989586621679458162 (Maybe (a6989586621679458163, b6989586621679458162)) -> Type) (l :: TyFun b6989586621679458162 [a6989586621679458163])
• type UnfoldrSym2 (t :: TyFun b6989586621679458162 (Maybe (a6989586621679458163, b6989586621679458162)) -> Type) (t :: b6989586621679458162) = Unfoldr t t
• data TakeSym0 (l :: TyFun Nat (TyFun [a6989586621679458094] [a6989586621679458094] -> Type))
• data TakeSym1 (l :: Nat) (l :: TyFun [a6989586621679458094] [a6989586621679458094])
• type TakeSym2 (t :: Nat) (t :: [a6989586621679458094]) = Take t t
• data DropSym0 (l :: TyFun Nat (TyFun [a6989586621679458093] [a6989586621679458093] -> Type))
• data DropSym1 (l :: Nat) (l :: TyFun [a6989586621679458093] [a6989586621679458093])
• type DropSym2 (t :: Nat) (t :: [a6989586621679458093]) = Drop t t
• data SplitAtSym0 (l :: TyFun Nat (TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]) -> Type))
• data SplitAtSym1 (l :: Nat) (l :: TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]))
• type SplitAtSym2 (t :: Nat) (t :: [a6989586621679458092]) = SplitAt t t
• data TakeWhileSym0 (l :: TyFun (TyFun a6989586621679458099 Bool -> Type) (TyFun [a6989586621679458099] [a6989586621679458099] -> Type))
• data TakeWhileSym1 (l :: TyFun a6989586621679458099 Bool -> Type) (l :: TyFun [a6989586621679458099] [a6989586621679458099])
• type TakeWhileSym2 (t :: TyFun a6989586621679458099 Bool -> Type) (t :: [a6989586621679458099]) = TakeWhile t t
• data DropWhileSym0 (l :: TyFun (TyFun a6989586621679458098 Bool -> Type) (TyFun [a6989586621679458098] [a6989586621679458098] -> Type))
• data DropWhileSym1 (l :: TyFun a6989586621679458098 Bool -> Type) (l :: TyFun [a6989586621679458098] [a6989586621679458098])
• type DropWhileSym2 (t :: TyFun a6989586621679458098 Bool -> Type) (t :: [a6989586621679458098]) = DropWhile t t
• data DropWhileEndSym0 (l :: TyFun (TyFun a6989586621679458097 Bool -> Type) (TyFun [a6989586621679458097] [a6989586621679458097] -> Type))
• data DropWhileEndSym1 (l :: TyFun a6989586621679458097 Bool -> Type) (l :: TyFun [a6989586621679458097] [a6989586621679458097])
• type DropWhileEndSym2 (t :: TyFun a6989586621679458097 Bool -> Type) (t :: [a6989586621679458097]) = DropWhileEnd t t
• data SpanSym0 (l :: TyFun (TyFun a6989586621679458096 Bool -> Type) (TyFun [a6989586621679458096] ([a6989586621679458096], [a6989586621679458096]) -> Type))
• data SpanSym1 (l :: TyFun a6989586621679458096 Bool -> Type) (l :: TyFun [a6989586621679458096] ([a6989586621679458096], [a6989586621679458096]))
• type SpanSym2 (t :: TyFun a6989586621679458096 Bool -> Type) (t :: [a6989586621679458096]) = Span t t
• data BreakSym0 (l :: TyFun (TyFun a6989586621679458095 Bool -> Type) (TyFun [a6989586621679458095] ([a6989586621679458095], [a6989586621679458095]) -> Type))
• data BreakSym1 (l :: TyFun a6989586621679458095 Bool -> Type) (l :: TyFun [a6989586621679458095] ([a6989586621679458095], [a6989586621679458095]))
• type BreakSym2 (t :: TyFun a6989586621679458095 Bool -> Type) (t :: [a6989586621679458095]) = Break t t
• data GroupSym0 (l :: TyFun [a6989586621679458091] [[a6989586621679458091]])
• type GroupSym1 (t :: [a6989586621679458091]) = Group t
• data InitsSym0 (l :: TyFun [a6989586621679458161] [[a6989586621679458161]])
• type InitsSym1 (t :: [a6989586621679458161]) = Inits t
• data TailsSym0 (l :: TyFun [a6989586621679458160] [[a6989586621679458160]])
• type TailsSym1 (t :: [a6989586621679458160]) = Tails t
• data IsPrefixOfSym0 (l :: TyFun [a6989586621679458159] (TyFun [a6989586621679458159] Bool -> Type))
• data IsPrefixOfSym1 (l :: [a6989586621679458159]) (l :: TyFun [a6989586621679458159] Bool)
• type IsPrefixOfSym2 (t :: [a6989586621679458159]) (t :: [a6989586621679458159]) = IsPrefixOf t t
• data IsSuffixOfSym0 (l :: TyFun [a6989586621679458158] (TyFun [a6989586621679458158] Bool -> Type))
• data IsSuffixOfSym1 (l :: [a6989586621679458158]) (l :: TyFun [a6989586621679458158] Bool)
• type IsSuffixOfSym2 (t :: [a6989586621679458158]) (t :: [a6989586621679458158]) = IsSuffixOf t t
• data IsInfixOfSym0 (l :: TyFun [a6989586621679458157] (TyFun [a6989586621679458157] Bool -> Type))
• data IsInfixOfSym1 (l :: [a6989586621679458157]) (l :: TyFun [a6989586621679458157] Bool)
• type IsInfixOfSym2 (t :: [a6989586621679458157]) (t :: [a6989586621679458157]) = IsInfixOf t t
• data ElemSym0 (l :: TyFun a6989586621679458156 (TyFun [a6989586621679458156] Bool -> Type))
• data ElemSym1 (l :: a6989586621679458156) (l :: TyFun [a6989586621679458156] Bool)
• type ElemSym2 (t :: a6989586621679458156) (t :: [a6989586621679458156]) = Elem t t
• data NotElemSym0 (l :: TyFun a6989586621679458155 (TyFun [a6989586621679458155] Bool -> Type))
• data NotElemSym1 (l :: a6989586621679458155) (l :: TyFun [a6989586621679458155] Bool)
• type NotElemSym2 (t :: a6989586621679458155) (t :: [a6989586621679458155]) = NotElem t t
• data LookupSym0 (l :: TyFun a6989586621679458084 (TyFun [(a6989586621679458084, b6989586621679458085)] (Maybe b6989586621679458085) -> Type))
• data LookupSym1 (l :: a6989586621679458084) (l :: TyFun [(a6989586621679458084, b6989586621679458085)] (Maybe b6989586621679458085))
• type LookupSym2 (t :: a6989586621679458084) (t :: [(a6989586621679458084, b6989586621679458085)]) = Lookup t t
• data FindSym0 (l :: TyFun (TyFun a6989586621679458106 Bool -> Type) (TyFun [a6989586621679458106] (Maybe a6989586621679458106) -> Type))
• data FindSym1 (l :: TyFun a6989586621679458106 Bool -> Type) (l :: TyFun [a6989586621679458106] (Maybe a6989586621679458106))
• type FindSym2 (t :: TyFun a6989586621679458106 Bool -> Type) (t :: [a6989586621679458106]) = Find t t
• data FilterSym0 (l :: TyFun (TyFun a6989586621679458107 Bool -> Type) (TyFun [a6989586621679458107] [a6989586621679458107] -> Type))
• data FilterSym1 (l :: TyFun a6989586621679458107 Bool -> Type) (l :: TyFun [a6989586621679458107] [a6989586621679458107])
• type FilterSym2 (t :: TyFun a6989586621679458107 Bool -> Type) (t :: [a6989586621679458107]) = Filter t t
• data PartitionSym0 (l :: TyFun (TyFun a6989586621679458083 Bool -> Type) (TyFun [a6989586621679458083] ([a6989586621679458083], [a6989586621679458083]) -> Type))
• data PartitionSym1 (l :: TyFun a6989586621679458083 Bool -> Type) (l :: TyFun [a6989586621679458083] ([a6989586621679458083], [a6989586621679458083]))
• type PartitionSym2 (t :: TyFun a6989586621679458083 Bool -> Type) (t :: [a6989586621679458083]) = Partition t t
• data (:!!$) (l :: TyFun [a6989586621679458076] (TyFun Nat a6989586621679458076 -> Type))
• data (l :: [a6989586621679458076]) :!!$$ (l :: TyFun Nat a6989586621679458076)
• type (:!!$$$) (t :: [a6989586621679458076]) (t :: Nat) = (:!!) t t
• data ElemIndexSym0 (l :: TyFun a6989586621679458105 (TyFun [a6989586621679458105] (Maybe Nat) -> Type))
• data ElemIndexSym1 (l :: a6989586621679458105) (l :: TyFun [a6989586621679458105] (Maybe Nat))
• type ElemIndexSym2 (t :: a6989586621679458105) (t :: [a6989586621679458105]) = ElemIndex t t
• data ElemIndicesSym0 (l :: TyFun a6989586621679458104 (TyFun [a6989586621679458104] [Nat] -> Type))
• data ElemIndicesSym1 (l :: a6989586621679458104) (l :: TyFun [a6989586621679458104] [Nat])
• type ElemIndicesSym2 (t :: a6989586621679458104) (t :: [a6989586621679458104]) = ElemIndices t t
• data FindIndexSym0 (l :: TyFun (TyFun a6989586621679458103 Bool -> Type) (TyFun [a6989586621679458103] (Maybe Nat) -> Type))
• data FindIndexSym1 (l :: TyFun a6989586621679458103 Bool -> Type) (l :: TyFun [a6989586621679458103] (Maybe Nat))
• type FindIndexSym2 (t :: TyFun a6989586621679458103 Bool -> Type) (t :: [a6989586621679458103]) = FindIndex t t
• data FindIndicesSym0 (l :: TyFun (TyFun a6989586621679458102 Bool -> Type) (TyFun [a6989586621679458102] [Nat] -> Type))
• data FindIndicesSym1 (l :: TyFun a6989586621679458102 Bool -> Type) (l :: TyFun [a6989586621679458102] [Nat])
• type FindIndicesSym2 (t :: TyFun a6989586621679458102 Bool -> Type) (t :: [a6989586621679458102]) = FindIndices t t
• data ZipSym0 (l :: TyFun [a6989586621679458153] (TyFun [b6989586621679458154] [(a6989586621679458153, b6989586621679458154)] -> Type))
• data ZipSym1 (l :: [a6989586621679458153]) (l :: TyFun [b6989586621679458154] [(a6989586621679458153, b6989586621679458154)])
• type ZipSym2 (t :: [a6989586621679458153]) (t :: [b6989586621679458154]) = Zip t t
• data Zip3Sym0 (l :: TyFun [a6989586621679458150] (TyFun [b6989586621679458151] (TyFun [c6989586621679458152] [(a6989586621679458150, b6989586621679458151, c6989586621679458152)] -> Type) -> Type))
• data Zip3Sym1 (l :: [a6989586621679458150]) (l :: TyFun [b6989586621679458151] (TyFun [c6989586621679458152] [(a6989586621679458150, b6989586621679458151, c6989586621679458152)] -> Type))
• data Zip3Sym2 (l :: [a6989586621679458150]) (l :: [b6989586621679458151]) (l :: TyFun [c6989586621679458152] [(a6989586621679458150, b6989586621679458151, c6989586621679458152)])
• type Zip3Sym3 (t :: [a6989586621679458150]) (t :: [b6989586621679458151]) (t :: [c6989586621679458152]) = Zip3 t t t
• data ZipWithSym0 (l :: TyFun (TyFun a6989586621679458147 (TyFun b6989586621679458148 c6989586621679458149 -> Type) -> Type) (TyFun [a6989586621679458147] (TyFun [b6989586621679458148] [c6989586621679458149] -> Type) -> Type))
• data ZipWithSym1 (l :: TyFun a6989586621679458147 (TyFun b6989586621679458148 c6989586621679458149 -> Type) -> Type) (l :: TyFun [a6989586621679458147] (TyFun [b6989586621679458148] [c6989586621679458149] -> Type))
• data ZipWithSym2 (l :: TyFun a6989586621679458147 (TyFun b6989586621679458148 c6989586621679458149 -> Type) -> Type) (l :: [a6989586621679458147]) (l :: TyFun [b6989586621679458148] [c6989586621679458149])
• type ZipWithSym3 (t :: TyFun a6989586621679458147 (TyFun b6989586621679458148 c6989586621679458149 -> Type) -> Type) (t :: [a6989586621679458147]) (t :: [b6989586621679458148]) = ZipWith t t t
• data ZipWith3Sym0 (l :: TyFun (TyFun a6989586621679458143 (TyFun b6989586621679458144 (TyFun c6989586621679458145 d6989586621679458146 -> Type) -> Type) -> Type) (TyFun [a6989586621679458143] (TyFun [b6989586621679458144] (TyFun [c6989586621679458145] [d6989586621679458146] -> Type) -> Type) -> Type))
• data ZipWith3Sym1 (l :: TyFun a6989586621679458143 (TyFun b6989586621679458144 (TyFun c6989586621679458145 d6989586621679458146 -> Type) -> Type) -> Type) (l :: TyFun [a6989586621679458143] (TyFun [b6989586621679458144] (TyFun [c6989586621679458145] [d6989586621679458146] -> Type) -> Type))
• data ZipWith3Sym2 (l :: TyFun a6989586621679458143 (TyFun b6989586621679458144 (TyFun c6989586621679458145 d6989586621679458146 -> Type) -> Type) -> Type) (l :: [a6989586621679458143]) (l :: TyFun [b6989586621679458144] (TyFun [c6989586621679458145] [d6989586621679458146] -> Type))
• data ZipWith3Sym3 (l :: TyFun a6989586621679458143 (TyFun b6989586621679458144 (TyFun c6989586621679458145 d6989586621679458146 -> Type) -> Type) -> Type) (l :: [a6989586621679458143]) (l :: [b6989586621679458144]) (l :: TyFun [c6989586621679458145] [d6989586621679458146])
• type ZipWith3Sym4 (t :: TyFun a6989586621679458143 (TyFun b6989586621679458144 (TyFun c6989586621679458145 d6989586621679458146 -> Type) -> Type) -> Type) (t :: [a6989586621679458143]) (t :: [b6989586621679458144]) (t :: [c6989586621679458145]) = ZipWith3 t t t t
• data UnzipSym0 (l :: TyFun [(a6989586621679458141, b6989586621679458142)] ([a6989586621679458141], [b6989586621679458142]))
• type UnzipSym1 (t :: [(a6989586621679458141, b6989586621679458142)]) = Unzip t
• data Unzip3Sym0 (l :: TyFun [(a6989586621679458138, b6989586621679458139, c6989586621679458140)] ([a6989586621679458138], [b6989586621679458139], [c6989586621679458140]))
• type Unzip3Sym1 (t :: [(a6989586621679458138, b6989586621679458139, c6989586621679458140)]) = Unzip3 t
• data Unzip4Sym0 (l :: TyFun [(a6989586621679458134, b6989586621679458135, c6989586621679458136, d6989586621679458137)] ([a6989586621679458134], [b6989586621679458135], [c6989586621679458136], [d6989586621679458137]))
• type Unzip4Sym1 (t :: [(a6989586621679458134, b6989586621679458135, c6989586621679458136, d6989586621679458137)]) = Unzip4 t
• data Unzip5Sym0 (l :: TyFun [(a6989586621679458129, b6989586621679458130, c6989586621679458131, d6989586621679458132, e6989586621679458133)] ([a6989586621679458129], [b6989586621679458130], [c6989586621679458131], [d6989586621679458132], [e6989586621679458133]))
• type Unzip5Sym1 (t :: [(a6989586621679458129, b6989586621679458130, c6989586621679458131, d6989586621679458132, e6989586621679458133)]) = Unzip5 t
• data Unzip6Sym0 (l :: TyFun [(a6989586621679458123, b6989586621679458124, c6989586621679458125, d6989586621679458126, e6989586621679458127, f6989586621679458128)] ([a6989586621679458123], [b6989586621679458124], [c6989586621679458125], [d6989586621679458126], [e6989586621679458127], [f6989586621679458128]))
• type Unzip6Sym1 (t :: [(a6989586621679458123, b6989586621679458124, c6989586621679458125, d6989586621679458126, e6989586621679458127, f6989586621679458128)]) = Unzip6 t
• data Unzip7Sym0 (l :: TyFun [(a6989586621679458116, b6989586621679458117, c6989586621679458118, d6989586621679458119, e6989586621679458120, f6989586621679458121, g6989586621679458122)] ([a6989586621679458116], [b6989586621679458117], [c6989586621679458118], [d6989586621679458119], [e6989586621679458120], [f6989586621679458121], [g6989586621679458122]))
• type Unzip7Sym1 (t :: [(a6989586621679458116, b6989586621679458117, c6989586621679458118, d6989586621679458119, e6989586621679458120, f6989586621679458121, g6989586621679458122)]) = Unzip7 t
• data NubSym0 (l :: TyFun [a6989586621679458075] [a6989586621679458075])
• type NubSym1 (t :: [a6989586621679458075]) = Nub t
• data DeleteSym0 (l :: TyFun a6989586621679458115 (TyFun [a6989586621679458115] [a6989586621679458115] -> Type))
• data DeleteSym1 (l :: a6989586621679458115) (l :: TyFun [a6989586621679458115] [a6989586621679458115])
• type DeleteSym2 (t :: a6989586621679458115) (t :: [a6989586621679458115]) = Delete t t
• data (:\\$) (l :: TyFun [a6989586621679458114] (TyFun [a6989586621679458114] [a6989586621679458114] -> Type))
• data (l :: [a6989586621679458114]) :\\$$ (l :: TyFun [a6989586621679458114] [a6989586621679458114])
• type (:\\$$$) (t :: [a6989586621679458114]) (t :: [a6989586621679458114]) = (:\\) t t
• data UnionSym0 (l :: TyFun [a6989586621679458071] (TyFun [a6989586621679458071] [a6989586621679458071] -> Type))
• data UnionSym1 (l :: [a6989586621679458071]) (l :: TyFun [a6989586621679458071] [a6989586621679458071])
• type UnionSym2 (t :: [a6989586621679458071]) (t :: [a6989586621679458071]) = Union t t
• data IntersectSym0 (l :: TyFun [a6989586621679458101] (TyFun [a6989586621679458101] [a6989586621679458101] -> Type))
• data IntersectSym1 (l :: [a6989586621679458101]) (l :: TyFun [a6989586621679458101] [a6989586621679458101])
• type IntersectSym2 (t :: [a6989586621679458101]) (t :: [a6989586621679458101]) = Intersect t t
• data InsertSym0 (l :: TyFun a6989586621679458088 (TyFun [a6989586621679458088] [a6989586621679458088] -> Type))
• data InsertSym1 (l :: a6989586621679458088) (l :: TyFun [a6989586621679458088] [a6989586621679458088])
• type InsertSym2 (t :: a6989586621679458088) (t :: [a6989586621679458088]) = Insert t t
• data SortSym0 (l :: TyFun [a6989586621679458087] [a6989586621679458087])
• type SortSym1 (t :: [a6989586621679458087]) = Sort t
• data NubBySym0 (l :: TyFun (TyFun a6989586621679458074 (TyFun a6989586621679458074 Bool -> Type) -> Type) (TyFun [a6989586621679458074] [a6989586621679458074] -> Type))
• data NubBySym1 (l :: TyFun a6989586621679458074 (TyFun a6989586621679458074 Bool -> Type) -> Type) (l :: TyFun [a6989586621679458074] [a6989586621679458074])
• type NubBySym2 (t :: TyFun a6989586621679458074 (TyFun a6989586621679458074 Bool -> Type) -> Type) (t :: [a6989586621679458074]) = NubBy t t
• data DeleteBySym0 (l :: TyFun (TyFun a6989586621679458113 (TyFun a6989586621679458113 Bool -> Type) -> Type) (TyFun a6989586621679458113 (TyFun [a6989586621679458113] [a6989586621679458113] -> Type) -> Type))
• data DeleteBySym1 (l :: TyFun a6989586621679458113 (TyFun a6989586621679458113 Bool -> Type) -> Type) (l :: TyFun a6989586621679458113 (TyFun [a6989586621679458113] [a6989586621679458113] -> Type))
• data DeleteBySym2 (l :: TyFun a6989586621679458113 (TyFun a6989586621679458113 Bool -> Type) -> Type) (l :: a6989586621679458113) (l :: TyFun [a6989586621679458113] [a6989586621679458113])
• type DeleteBySym3 (t :: TyFun a6989586621679458113 (TyFun a6989586621679458113 Bool -> Type) -> Type) (t :: a6989586621679458113) (t :: [a6989586621679458113]) = DeleteBy t t t
• data DeleteFirstsBySym0 (l :: TyFun (TyFun a6989586621679458112 (TyFun a6989586621679458112 Bool -> Type) -> Type) (TyFun [a6989586621679458112] (TyFun [a6989586621679458112] [a6989586621679458112] -> Type) -> Type))
• data DeleteFirstsBySym1 (l :: TyFun a6989586621679458112 (TyFun a6989586621679458112 Bool -> Type) -> Type) (l :: TyFun [a6989586621679458112] (TyFun [a6989586621679458112] [a6989586621679458112] -> Type))
• data DeleteFirstsBySym2 (l :: TyFun a6989586621679458112 (TyFun a6989586621679458112 Bool -> Type) -> Type) (l :: [a6989586621679458112]) (l :: TyFun [a6989586621679458112] [a6989586621679458112])
• type DeleteFirstsBySym3 (t :: TyFun a6989586621679458112 (TyFun a6989586621679458112 Bool -> Type) -> Type) (t :: [a6989586621679458112]) (t :: [a6989586621679458112]) = DeleteFirstsBy t t t
• data UnionBySym0 (l :: TyFun (TyFun a6989586621679458072 (TyFun a6989586621679458072 Bool -> Type) -> Type) (TyFun [a6989586621679458072] (TyFun [a6989586621679458072] [a6989586621679458072] -> Type) -> Type))
• data UnionBySym1 (l :: TyFun a6989586621679458072 (TyFun a6989586621679458072 Bool -> Type) -> Type) (l :: TyFun [a6989586621679458072] (TyFun [a6989586621679458072] [a6989586621679458072] -> Type))
• data UnionBySym2 (l :: TyFun a6989586621679458072 (TyFun a6989586621679458072 Bool -> Type) -> Type) (l :: [a6989586621679458072]) (l :: TyFun [a6989586621679458072] [a6989586621679458072])
• type UnionBySym3 (t :: TyFun a6989586621679458072 (TyFun a6989586621679458072 Bool -> Type) -> Type) (t :: [a6989586621679458072]) (t :: [a6989586621679458072]) = UnionBy t t t
• data IntersectBySym0 (l :: TyFun (TyFun a6989586621679458100 (TyFun a6989586621679458100 Bool -> Type) -> Type) (TyFun [a6989586621679458100] (TyFun [a6989586621679458100] [a6989586621679458100] -> Type) -> Type))
• data IntersectBySym1 (l :: TyFun a6989586621679458100 (TyFun a6989586621679458100 Bool -> Type) -> Type) (l :: TyFun [a6989586621679458100] (TyFun [a6989586621679458100] [a6989586621679458100] -> Type))
• data IntersectBySym2 (l :: TyFun a6989586621679458100 (TyFun a6989586621679458100 Bool -> Type) -> Type) (l :: [a6989586621679458100]) (l :: TyFun [a6989586621679458100] [a6989586621679458100])
• type IntersectBySym3 (t :: TyFun a6989586621679458100 (TyFun a6989586621679458100 Bool -> Type) -> Type) (t :: [a6989586621679458100]) (t :: [a6989586621679458100]) = IntersectBy t t t
• data GroupBySym0 (l :: TyFun (TyFun a6989586621679458086 (TyFun a6989586621679458086 Bool -> Type) -> Type) (TyFun [a6989586621679458086] [[a6989586621679458086]] -> Type))
• data GroupBySym1 (l :: TyFun a6989586621679458086 (TyFun a6989586621679458086 Bool -> Type) -> Type) (l :: TyFun [a6989586621679458086] [[a6989586621679458086]])
• type GroupBySym2 (t :: TyFun a6989586621679458086 (TyFun a6989586621679458086 Bool -> Type) -> Type) (t :: [a6989586621679458086]) = GroupBy t t
• data SortBySym0 (l :: TyFun (TyFun a6989586621679458111 (TyFun a6989586621679458111 Ordering -> Type) -> Type) (TyFun [a6989586621679458111] [a6989586621679458111] -> Type))
• data SortBySym1 (l :: TyFun a6989586621679458111 (TyFun a6989586621679458111 Ordering -> Type) -> Type) (l :: TyFun [a6989586621679458111] [a6989586621679458111])
• type SortBySym2 (t :: TyFun a6989586621679458111 (TyFun a6989586621679458111 Ordering -> Type) -> Type) (t :: [a6989586621679458111]) = SortBy t t
• data InsertBySym0 (l :: TyFun (TyFun a6989586621679458110 (TyFun a6989586621679458110 Ordering -> Type) -> Type) (TyFun a6989586621679458110 (TyFun [a6989586621679458110] [a6989586621679458110] -> Type) -> Type))
• data InsertBySym1 (l :: TyFun a6989586621679458110 (TyFun a6989586621679458110 Ordering -> Type) -> Type) (l :: TyFun a6989586621679458110 (TyFun [a6989586621679458110] [a6989586621679458110] -> Type))
• data InsertBySym2 (l :: TyFun a6989586621679458110 (TyFun a6989586621679458110 Ordering -> Type) -> Type) (l :: a6989586621679458110) (l :: TyFun [a6989586621679458110] [a6989586621679458110])
• type InsertBySym3 (t :: TyFun a6989586621679458110 (TyFun a6989586621679458110 Ordering -> Type) -> Type) (t :: a6989586621679458110) (t :: [a6989586621679458110]) = InsertBy t t t
• data MaximumBySym0 (l :: TyFun (TyFun a6989586621679458109 (TyFun a6989586621679458109 Ordering -> Type) -> Type) (TyFun [a6989586621679458109] a6989586621679458109 -> Type))
• data MaximumBySym1 (l :: TyFun a6989586621679458109 (TyFun a6989586621679458109 Ordering -> Type) -> Type) (l :: TyFun [a6989586621679458109] a6989586621679458109)
• type MaximumBySym2 (t :: TyFun a6989586621679458109 (TyFun a6989586621679458109 Ordering -> Type) -> Type) (t :: [a6989586621679458109]) = MaximumBy t t
• data MinimumBySym0 (l :: TyFun (TyFun a6989586621679458108 (TyFun a6989586621679458108 Ordering -> Type) -> Type) (TyFun [a6989586621679458108] a6989586621679458108 -> Type))
• data MinimumBySym1 (l :: TyFun a6989586621679458108 (TyFun a6989586621679458108 Ordering -> Type) -> Type) (l :: TyFun [a6989586621679458108] a6989586621679458108)
• type MinimumBySym2 (t :: TyFun a6989586621679458108 (TyFun a6989586621679458108 Ordering -> Type) -> Type) (t :: [a6989586621679458108]) = MinimumBy t t
• data GenericLengthSym0 (l :: TyFun [a6989586621679458070] i6989586621679458069)
• type GenericLengthSym1 (t :: [a6989586621679458070]) = GenericLength t

The singleton for lists

SNil  :: Sing '[]
SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)

Basic functions

List transformations

Reducing lists (folds)

Special folds

Building lists

Scans

Accumulating maps

Cyclical lists

Unfolding

Sublists

Extracting sublists

Predicates

Searching lists

Searching by equality

Searching with a predicate

Indexing lists

Zipping and unzipping lists

Special lists

"Set" operations

Ordered lists

Generalized functions

The "By" operations

User-supplied equality (replacing an Eq context)

User-supplied comparison (replacing an Ord context)

The "generic" operations

Defunctionalization symbols