Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.List1

Description

Non-empty lists.

Better name List1 for non-empty lists, plus missing functionality.

Import: @

{-# LANGUAGE PatternSynonyms #-}

import Agda.Utils.List1 (List1, pattern (:|)) import qualified Agda.Utils.List1 as List1

@

Synopsis

Documentation

catMaybes :: List1 (Maybe a) -> [a] Source #

Like catMaybes.

zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c) Source #

Like zipWithM.

partitionEithers :: List1 (Either a b) -> ([a], [b]) Source #

zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m () Source #

Like zipWithM.

type String1 = List1 Char Source #

ifNull :: [a] -> b -> (List1 a -> b) -> b Source #

union :: Eq a => List1 a -> List1 a -> List1 a Source #

Like union. Duplicates in the first list are not removed. O(nm).

mapMaybe :: (a -> Maybe b) -> List1 a -> [b] Source #

Like mapMaybe.

initLast :: List1 a -> ([a], a) Source #

Return the last element and the rest.

find :: (a -> Bool) -> List1 a -> Maybe a Source #

Like find.

lefts :: List1 (Either a b) -> [a] Source #

Like lefts.

snoc :: [a] -> a -> List1 a Source #

Build a list with one element.

More precise type for snoc.

updateHead :: (a -> a) -> List1 a -> List1 a Source #

Update the first element of a non-empty list. O(1).

updateLast :: (a -> a) -> List1 a -> List1 a Source #

Update the last element of a non-empty list. O(n).

concat :: [List1 a] -> [a] Source #

Concatenate one or more non-empty lists.

unwords :: List1 String -> String Source #

Like unwords.

foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b Source #

List foldr but with a base case for the singleton list.

rights :: List1 (Either a b) -> [b] Source #

Like rights.

last2 :: List1 a -> Maybe (a, a) Source #

Last two elements (safe). O(n).

ifNotNull :: [a] -> (List1 a -> b) -> b -> b Source #

unlessNull :: Null m => [a] -> (List1 a -> m) -> m Source #

liftList1 :: (List1 a -> List1 b) -> [a] -> [b] Source #

Lift a function on non-empty lists to a function on lists.

This is in essence fmap for Maybe, if we take [a] = Maybe (List1 a).

breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a]) Source #

Breaks a list just after an element satisfying the predicate is found.

>>> breakAfter even [1,3,5,2,4,7,8]
(1 :| [3,5,2],[4,7,8])

allEqual :: Eq a => List1 a -> Bool Source #

Checks if all the elements in the list are equal. Assumes that the Eq instance stands for an equivalence relation. O(n).

nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a) Source #

Non-efficient, monadic nub. O(n²).

wordsBy :: (a -> Bool) -> [a] -> [List1 a] Source #

Split a list into sublists. Generalisation of the prelude function words. Same as wordsBy and wordsBy, but with the non-emptyness guarantee on the chunks. O(n).

words xs == wordsBy isSpace xs

toList' :: Maybe (List1 a) -> [a] Source #

Lossless toList, opposite of nonEmpty.

fromListSafe Source #

Arguments

:: List1 a

Default value if convertee is empty.

-> [a]

List to convert, supposedly non-empty.

-> List1 a

Converted list.

Safe version of fromList.

groupOn :: Ord b => (a -> b) -> [a] -> [List1 a] Source #

groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f). O(n log n).

groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a) Source #

groupBy' :: (a -> a -> Bool) -> [a] -> [List1 a] Source #

More precise type for groupBy'.

A variant of groupBy which applies the predicate to consecutive pairs. O(n).

groupByFst :: Eq a => [(a, b)] -> [(a, List1 b)] Source #

Group consecutive items that share the same first component.

groupByFst1 :: Eq a => List1 (a, b) -> List1 (a, List1 b) Source #

Group consecutive items that share the same first component.

concatMap1 :: (a -> List1 b) -> List1 a -> List1 b Source #

lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a) Source #

Focus on the first element of a non-empty list. O(1).

lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a) Source #

Focus on the last element of a non-empty list. O(n).

xor :: NonEmpty Bool -> Bool #

data NonEmpty a #

Constructors

a :| [a] 

Instances

Instances details
NumHoles NameParts Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: NameParts -> Int Source #

MonadZip NonEmpty 
Instance details

Defined in Control.Monad.Zip

Methods

mzip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b)

mzipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c

munzip :: NonEmpty (a, b) -> (NonEmpty a, NonEmpty b)

Foldable1 NonEmpty 
Instance details

Defined in Data.Foldable1

Methods

fold1 :: Semigroup m => NonEmpty m -> m

foldMap1 :: Semigroup m => (a -> m) -> NonEmpty a -> m

foldMap1' :: Semigroup m => (a -> m) -> NonEmpty a -> m

toNonEmpty :: NonEmpty a -> NonEmpty a

maximum :: Ord a => NonEmpty a -> a

minimum :: Ord a => NonEmpty a -> a

head :: NonEmpty a -> a

last :: NonEmpty a -> a

foldrMap1 :: (a -> b) -> (a -> b -> b) -> NonEmpty a -> b

foldlMap1' :: (a -> b) -> (b -> a -> b) -> NonEmpty a -> b

foldlMap1 :: (a -> b) -> (b -> a -> b) -> NonEmpty a -> b

foldrMap1' :: (a -> b) -> (a -> b -> b) -> NonEmpty a -> b

Eq1 NonEmpty 
Instance details

Defined in Data.Functor.Classes

Methods

liftEq :: (a -> b -> Bool) -> NonEmpty a -> NonEmpty b -> Bool

Ord1 NonEmpty 
Instance details

Defined in Data.Functor.Classes

Methods

liftCompare :: (a -> b -> Ordering) -> NonEmpty a -> NonEmpty b -> Ordering

Read1 NonEmpty 
Instance details

Defined in Data.Functor.Classes

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (NonEmpty a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [NonEmpty a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (NonEmpty a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [NonEmpty a]

Show1 NonEmpty 
Instance details

Defined in Data.Functor.Classes

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> NonEmpty a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [NonEmpty a] -> ShowS

NFData1 NonEmpty 
Instance details

Defined in Control.DeepSeq

Methods

liftRnf :: (a -> ()) -> NonEmpty a -> ()

Applicative NonEmpty 
Instance details

Defined in GHC.Internal.Base

Methods

pure :: a -> NonEmpty a

(<*>) :: NonEmpty (a -> b) -> NonEmpty a -> NonEmpty b #

liftA2 :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c

(*>) :: NonEmpty a -> NonEmpty b -> NonEmpty b

(<*) :: NonEmpty a -> NonEmpty b -> NonEmpty a

Functor NonEmpty 
Instance details

Defined in GHC.Internal.Base

Methods

fmap :: (a -> b) -> NonEmpty a -> NonEmpty b

(<$) :: a -> NonEmpty b -> NonEmpty a #

Monad NonEmpty 
Instance details

Defined in GHC.Internal.Base

Methods

(>>=) :: NonEmpty a -> (a -> NonEmpty b) -> NonEmpty b

(>>) :: NonEmpty a -> NonEmpty b -> NonEmpty b

return :: a -> NonEmpty a

MonadFix NonEmpty 
Instance details

Defined in GHC.Internal.Control.Monad.Fix

Methods

mfix :: (a -> NonEmpty a) -> NonEmpty a

Foldable NonEmpty 
Instance details

Defined in GHC.Internal.Data.Foldable

Methods

fold :: Monoid m => NonEmpty m -> m

foldMap :: Monoid m => (a -> m) -> NonEmpty a -> m

foldMap' :: Monoid m => (a -> m) -> NonEmpty a -> m

foldr :: (a -> b -> b) -> b -> NonEmpty a -> b

foldr' :: (a -> b -> b) -> b -> NonEmpty a -> b

foldl :: (b -> a -> b) -> b -> NonEmpty a -> b

foldl' :: (b -> a -> b) -> b -> NonEmpty a -> b

foldr1 :: (a -> a -> a) -> NonEmpty a -> a

foldl1 :: (a -> a -> a) -> NonEmpty a -> a

toList :: NonEmpty a -> [a]

null :: NonEmpty a -> Bool

length :: NonEmpty a -> Int

elem :: Eq a => a -> NonEmpty a -> Bool

maximum :: Ord a => NonEmpty a -> a

minimum :: Ord a => NonEmpty a -> a

sum :: Num a => NonEmpty a -> a

product :: Num a => NonEmpty a -> a

IsString String1 
Instance details

Defined in Agda.Utils.String

Methods

fromString :: String -> String1

Traversable NonEmpty 
Instance details

Defined in GHC.Internal.Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)

sequenceA :: Applicative f => NonEmpty (f a) -> f (NonEmpty a)

mapM :: Monad m => (a -> m b) -> NonEmpty a -> m (NonEmpty b)

sequence :: Monad m => NonEmpty (m a) -> m (NonEmpty a)

Hashable1 NonEmpty 
Instance details

Defined in Data.Hashable.Class

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> NonEmpty a -> Int

FromJSON1 NonEmpty 
Instance details

Defined in Data.Aeson.Types.FromJSON

Methods

liftParseJSON :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser (NonEmpty a) #

liftParseJSONList :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser [NonEmpty a] #

liftOmittedField :: Maybe a -> Maybe (NonEmpty a) #

ToJSON1 NonEmpty 
Instance details

Defined in Data.Aeson.Types.ToJSON

Methods

liftToJSON :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> NonEmpty a -> Value #

liftToJSONList :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> [NonEmpty a] -> Value #

liftToEncoding :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> NonEmpty a -> Encoding #

liftToEncodingList :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> [NonEmpty a] -> Encoding #

liftOmitField :: (a -> Bool) -> NonEmpty a -> Bool #

Generic1 NonEmpty 
Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep1 NonEmpty 
Instance details

Defined in GHC.Internal.Generics

type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Internal.Base" "ghc-internal" 'False) (C1 ('MetaCons ":|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 [])))

Methods

from1 :: NonEmpty a -> Rep1 NonEmpty a

to1 :: Rep1 NonEmpty a -> NonEmpty a

Singleton a (NonEmpty a) Source # 
Instance details

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> NonEmpty a Source #

Lift a => Lift (NonEmpty a :: Type) 
Instance details

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Quote m => NonEmpty a -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => NonEmpty a -> Code m (NonEmpty a)

Pretty a => Pretties (List1 a) Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretties :: (Nat, Bool, JSModuleStyle) -> List1 a -> [Doc] Source #

SubstExpr a => SubstExpr (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> List1 a -> List1 a Source #

DeclaredNames a => DeclaredNames (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => List1 a -> m Source #

ExprLike a => ExprLike (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Pretty a => Pretty (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: List1 a -> Doc Source #

prettyPrec :: Int -> List1 a -> Doc Source #

prettyList :: [List1 a] -> Doc Source #

ExprLike a => ExprLike (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> List1 a -> List1 a Source #

foldExpr :: Monoid m => (Expr -> m) -> List1 a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> List1 a -> m (List1 a) Source #

FoldDecl a => FoldDecl (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

foldDecl :: Monoid m => (Declaration -> m) -> List1 a -> m Source #

TraverseDecl a => TraverseDecl (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> List1 a -> m (List1 a) Source #

CPatternLike p => CPatternLike (List1 p) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> List1 p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> List1 p -> m (List1 p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> List1 p -> m (List1 p) Source #

NamesIn a => NamesIn (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> List1 a -> m Source #

HasRange a => HasRange (List1 a) Source #

Precondition: The ranges of the list elements must point to the same file (or be empty).

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: List1 a -> Range Source #

KillRange a => KillRange (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Position

SetBindingSite a => SetBindingSite (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> List1 a -> List1 a Source #

ToConcrete a => ToConcrete (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a) 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (List1 a) = List1 (ConOfAbs a)
ToAbstract c => ToAbstract (List1 c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (List1 c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (List1 c) = List1 (AbsOfCon c)
ToAbstract (List1 (QNamed Clause)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause)) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

EmbPrj a => EmbPrj (List1 a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: List1 a -> S Int32 Source #

icod_ :: List1 a -> S Int32 Source #

value :: Int32 -> R (List1 a) Source #

Sized (List1 a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: List1 a -> Int Source #

natSize :: List1 a -> Peano Source #

Binary a => Binary (NonEmpty a) 
Instance details

Defined in Data.Binary.Class

Methods

put :: NonEmpty a -> Put

get :: Get (NonEmpty a)

putList :: [NonEmpty a] -> Put

ToMarkup (NonEmpty Char) 
Instance details

Defined in Text.Blaze

Methods

toMarkup :: NonEmpty Char -> Markup

preEscapedToMarkup :: NonEmpty Char -> Markup

ToValue (NonEmpty Char) 
Instance details

Defined in Text.Blaze

Methods

toValue :: NonEmpty Char -> AttributeValue

preEscapedToValue :: NonEmpty Char -> AttributeValue

NFData a => NFData (NonEmpty a) 
Instance details

Defined in Control.DeepSeq

Methods

rnf :: NonEmpty a -> ()

Semigroup (NonEmpty a) 
Instance details

Defined in GHC.Internal.Base

Methods

(<>) :: NonEmpty a -> NonEmpty a -> NonEmpty a #

sconcat :: NonEmpty (NonEmpty a) -> NonEmpty a

stimes :: Integral b => b -> NonEmpty a -> NonEmpty a

Generic (NonEmpty a) 
Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep (NonEmpty a) 
Instance details

Defined in GHC.Internal.Generics

type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Internal.Base" "ghc-internal" 'False) (C1 ('MetaCons ":|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

Methods

from :: NonEmpty a -> Rep (NonEmpty a) x

to :: Rep (NonEmpty a) x -> NonEmpty a

IsList (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

type Item (NonEmpty a) = a

Methods

fromList :: [Item (NonEmpty a)] -> NonEmpty a #

fromListN :: Int -> [Item (NonEmpty a)] -> NonEmpty a #

toList :: NonEmpty a -> [Item (NonEmpty a)] #

Read a => Read (NonEmpty a) 
Instance details

Defined in GHC.Internal.Read

Methods

readsPrec :: Int -> ReadS (NonEmpty a)

readList :: ReadS [NonEmpty a]

readPrec :: ReadPrec (NonEmpty a)

readListPrec :: ReadPrec [NonEmpty a]

Show a => Show (NonEmpty a) 
Instance details

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> NonEmpty a -> ShowS

show :: NonEmpty a -> String

showList :: [NonEmpty a] -> ShowS

Eq a => Eq (NonEmpty a) 
Instance details

Defined in GHC.Internal.Base

Methods

(==) :: NonEmpty a -> NonEmpty a -> Bool

(/=) :: NonEmpty a -> NonEmpty a -> Bool

Ord a => Ord (NonEmpty a) 
Instance details

Defined in GHC.Internal.Base

Methods

compare :: NonEmpty a -> NonEmpty a -> Ordering

(<) :: NonEmpty a -> NonEmpty a -> Bool

(<=) :: NonEmpty a -> NonEmpty a -> Bool

(>) :: NonEmpty a -> NonEmpty a -> Bool

(>=) :: NonEmpty a -> NonEmpty a -> Bool

max :: NonEmpty a -> NonEmpty a -> NonEmpty a

min :: NonEmpty a -> NonEmpty a -> NonEmpty a

Hashable a => Hashable (NonEmpty a) 
Instance details

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> NonEmpty a -> Int

hash :: NonEmpty a -> Int

FromJSON a => FromJSON (NonEmpty a) 
Instance details

Defined in Data.Aeson.Types.FromJSON

Methods

parseJSON :: Value -> Parser (NonEmpty a) #

parseJSONList :: Value -> Parser [NonEmpty a] #

omittedField :: Maybe (NonEmpty a) #

ToJSON a => ToJSON (NonEmpty a) 
Instance details

Defined in Data.Aeson.Types.ToJSON

AddContext (List1 Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (Arg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source #

contextSize :: (List1 (Arg Name), Type) -> Nat Source #

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (WithHiding Name), Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

type Rep1 NonEmpty 
Instance details

Defined in GHC.Internal.Generics

type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Internal.Base" "ghc-internal" 'False) (C1 ('MetaCons ":|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1 :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 [])))
type ConOfAbs (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (List1 a) = List1 (ConOfAbs a)
type AbsOfCon (List1 c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (List1 c) = List1 (AbsOfCon c)
type AbsOfRef (List1 (QNamed Clause)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type Rep (NonEmpty a) 
Instance details

Defined in GHC.Internal.Generics

type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Internal.Base" "ghc-internal" 'False) (C1 ('MetaCons ":|" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))
type Item (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

type Item (NonEmpty a) = a

group :: (Foldable f, Eq a) => f a -> [NonEmpty a] #

(!!) :: HasCallStack => NonEmpty a -> Int -> a #

sortBy :: (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a #

isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool #

partition :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #

singleton :: a -> NonEmpty a #

(<|) :: a -> NonEmpty a -> NonEmpty a #

map :: (a -> b) -> NonEmpty a -> NonEmpty b #

insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a #

sort :: Ord a => NonEmpty a -> NonEmpty a #

sortOn :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty a #

head :: NonEmpty a -> a #

length :: NonEmpty a -> Int #

nonEmpty :: [a] -> Maybe (NonEmpty a) #

tails :: Foldable f => f a -> NonEmpty [a] #

unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b #

filter :: (a -> Bool) -> NonEmpty a -> [a] #

drop :: Int -> NonEmpty a -> [a] #

splitAt :: Int -> NonEmpty a -> ([a], [a]) #

break :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #

dropWhile :: (a -> Bool) -> NonEmpty a -> [a] #

init :: NonEmpty a -> [a] #

iterate :: (a -> a) -> a -> NonEmpty a #

last :: NonEmpty a -> a #

repeat :: a -> NonEmpty a #

scanl :: Foldable f => (b -> a -> b) -> b -> f a -> NonEmpty b #

scanl1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a #

scanr :: Foldable f => (a -> b -> b) -> b -> f a -> NonEmpty b #

scanr1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a #

span :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #

tail :: NonEmpty a -> [a] #

take :: Int -> NonEmpty a -> [a] #

takeWhile :: (a -> Bool) -> NonEmpty a -> [a] #

zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c #

zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b) #

cons :: a -> NonEmpty a -> NonEmpty a #

uncons :: NonEmpty a -> (a, Maybe (NonEmpty a)) #

groupBy :: Foldable f => (a -> a -> Bool) -> f a -> [NonEmpty a] #

inits :: Foldable f => f a -> NonEmpty [a] #

nub :: Eq a => NonEmpty a -> NonEmpty a #

nubBy :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty a #

permutations :: [a] -> NonEmpty [a] #

unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b #

groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [NonEmpty a] #

sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a #

appendList :: NonEmpty a -> [a] -> NonEmpty a #

group1 :: Eq a => NonEmpty a -> NonEmpty (NonEmpty a) #

groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a] #

groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #

groupBy1 :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a) #

groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #

prependList :: [a] -> NonEmpty a -> NonEmpty a #

some1 :: Alternative f => f a -> f (NonEmpty a) #

class IsList l where #

Minimal complete definition

fromList, toList

Associated Types

type Item l #

Methods

fromList :: [Item l] -> l #

fromListN :: Int -> [Item l] -> l #

toList :: l -> [Item l] #

Instances

Instances details
IsList ByteArray 
Instance details

Defined in Data.Array.Byte

Associated Types

type Item ByteArray 
Instance details

Defined in Data.Array.Byte

type Item ByteArray = Word8

Methods

fromList :: [Item ByteArray] -> ByteArray #

fromListN :: Int -> [Item ByteArray] -> ByteArray #

toList :: ByteArray -> [Item ByteArray] #

IsList ByteString 
Instance details

Defined in Data.ByteString.Internal.Type

Associated Types

type Item ByteString 
Instance details

Defined in Data.ByteString.Internal.Type

type Item ByteString = Word8

Methods

fromList :: [Item ByteString] -> ByteString #

fromListN :: Int -> [Item ByteString] -> ByteString #

toList :: ByteString -> [Item ByteString] #

IsList ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

Associated Types

type Item ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

type Item ByteString = Word8

Methods

fromList :: [Item ByteString] -> ByteString #

fromListN :: Int -> [Item ByteString] -> ByteString #

toList :: ByteString -> [Item ByteString] #

IsList ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

Associated Types

type Item ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

type Item ShortByteString = Word8

Methods

fromList :: [Item ShortByteString] -> ShortByteString #

fromListN :: Int -> [Item ShortByteString] -> ShortByteString #

toList :: ShortByteString -> [Item ShortByteString] #

IsList IntSet 
Instance details

Defined in Data.IntSet.Internal

Associated Types

type Item IntSet 
Instance details

Defined in Data.IntSet.Internal

type Item IntSet = Key

Methods

fromList :: [Item IntSet] -> IntSet #

fromListN :: Int -> [Item IntSet] -> IntSet #

toList :: IntSet -> [Item IntSet] #

IsList Version 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item Version 
Instance details

Defined in GHC.Internal.IsList

type Item Version = Int

Methods

fromList :: [Item Version] -> Version #

fromListN :: Int -> [Item Version] -> Version #

toList :: Version -> [Item Version] #

IsList CallStack 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item CallStack 
Instance details

Defined in GHC.Internal.IsList

type Item CallStack = (String, SrcLoc)
IsList ShortText 
Instance details

Defined in Data.Text.Short.Internal

Associated Types

type Item ShortText 
Instance details

Defined in Data.Text.Short.Internal

type Item ShortText = Char

Methods

fromList :: [Item ShortText] -> ShortText #

fromListN :: Int -> [Item ShortText] -> ShortText #

toList :: ShortText -> [Item ShortText] #

IsList (List2 a) Source #

fromList is unsafe.

Instance details

Defined in Agda.Utils.List2

Associated Types

type Item (List2 a) 
Instance details

Defined in Agda.Utils.List2

type Item (List2 a) = a

Methods

fromList :: [Item (List2 a)] -> List2 a #

fromListN :: Int -> [Item (List2 a)] -> List2 a #

toList :: List2 a -> [Item (List2 a)] #

IsList (IntMap a) 
Instance details

Defined in Data.IntMap.Internal

Associated Types

type Item (IntMap a) 
Instance details

Defined in Data.IntMap.Internal

type Item (IntMap a) = (Key, a)

Methods

fromList :: [Item (IntMap a)] -> IntMap a #

fromListN :: Int -> [Item (IntMap a)] -> IntMap a #

toList :: IntMap a -> [Item (IntMap a)] #

IsList (Seq a) 
Instance details

Defined in Data.Sequence.Internal

Associated Types

type Item (Seq a) 
Instance details

Defined in Data.Sequence.Internal

type Item (Seq a) = a

Methods

fromList :: [Item (Seq a)] -> Seq a #

fromListN :: Int -> [Item (Seq a)] -> Seq a #

toList :: Seq a -> [Item (Seq a)] #

Ord a => IsList (Set a) 
Instance details

Defined in Data.Set.Internal

Associated Types

type Item (Set a) 
Instance details

Defined in Data.Set.Internal

type Item (Set a) = a

Methods

fromList :: [Item (Set a)] -> Set a #

fromListN :: Int -> [Item (Set a)] -> Set a #

toList :: Set a -> [Item (Set a)] #

IsList (DNonEmpty a) 
Instance details

Defined in Data.DList.DNonEmpty.Internal

Associated Types

type Item (DNonEmpty a) 
Instance details

Defined in Data.DList.DNonEmpty.Internal

type Item (DNonEmpty a) = a

Methods

fromList :: [Item (DNonEmpty a)] -> DNonEmpty a #

fromListN :: Int -> [Item (DNonEmpty a)] -> DNonEmpty a #

toList :: DNonEmpty a -> [Item (DNonEmpty a)] #

IsList (DList a) 
Instance details

Defined in Data.DList.Internal

Associated Types

type Item (DList a) 
Instance details

Defined in Data.DList.Internal

type Item (DList a) = a

Methods

fromList :: [Item (DList a)] -> DList a #

fromListN :: Int -> [Item (DList a)] -> DList a #

toList :: DList a -> [Item (DList a)] #

IsList (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

type Item (NonEmpty a) = a

Methods

fromList :: [Item (NonEmpty a)] -> NonEmpty a #

fromListN :: Int -> [Item (NonEmpty a)] -> NonEmpty a #

toList :: NonEmpty a -> [Item (NonEmpty a)] #

IsList (ZipList a) 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item (ZipList a) 
Instance details

Defined in GHC.Internal.IsList

type Item (ZipList a) = a

Methods

fromList :: [Item (ZipList a)] -> ZipList a #

fromListN :: Int -> [Item (ZipList a)] -> ZipList a #

toList :: ZipList a -> [Item (ZipList a)] #

(Eq a, Hashable a) => IsList (HashSet a) 
Instance details

Defined in Data.HashSet.Internal

Associated Types

type Item (HashSet a) 
Instance details

Defined in Data.HashSet.Internal

type Item (HashSet a) = a

Methods

fromList :: [Item (HashSet a)] -> HashSet a #

fromListN :: Int -> [Item (HashSet a)] -> HashSet a #

toList :: HashSet a -> [Item (HashSet a)] #

IsList (Array a) 
Instance details

Defined in Data.Primitive.Array

Associated Types

type Item (Array a) 
Instance details

Defined in Data.Primitive.Array

type Item (Array a) = a

Methods

fromList :: [Item (Array a)] -> Array a #

fromListN :: Int -> [Item (Array a)] -> Array a #

toList :: Array a -> [Item (Array a)] #

Prim a => IsList (PrimArray a) 
Instance details

Defined in Data.Primitive.PrimArray

Associated Types

type Item (PrimArray a) 
Instance details

Defined in Data.Primitive.PrimArray

type Item (PrimArray a) = a

Methods

fromList :: [Item (PrimArray a)] -> PrimArray a #

fromListN :: Int -> [Item (PrimArray a)] -> PrimArray a #

toList :: PrimArray a -> [Item (PrimArray a)] #

IsList (SmallArray a) 
Instance details

Defined in Data.Primitive.SmallArray

Associated Types

type Item (SmallArray a) 
Instance details

Defined in Data.Primitive.SmallArray

type Item (SmallArray a) = a

Methods

fromList :: [Item (SmallArray a)] -> SmallArray a #

fromListN :: Int -> [Item (SmallArray a)] -> SmallArray a #

toList :: SmallArray a -> [Item (SmallArray a)] #

IsList (KeyMap v) 
Instance details

Defined in Data.Aeson.KeyMap

Associated Types

type Item (KeyMap v) 
Instance details

Defined in Data.Aeson.KeyMap

type Item (KeyMap v) = (Key, v)

Methods

fromList :: [Item (KeyMap v)] -> KeyMap v #

fromListN :: Int -> [Item (KeyMap v)] -> KeyMap v #

toList :: KeyMap v -> [Item (KeyMap v)] #

IsList (Vector a) 
Instance details

Defined in Data.Vector

Associated Types

type Item (Vector a) 
Instance details

Defined in Data.Vector

type Item (Vector a) = a

Methods

fromList :: [Item (Vector a)] -> Vector a #

fromListN :: Int -> [Item (Vector a)] -> Vector a #

toList :: Vector a -> [Item (Vector a)] #

Prim a => IsList (Vector a) 
Instance details

Defined in Data.Vector.Primitive

Associated Types

type Item (Vector a) 
Instance details

Defined in Data.Vector.Primitive

type Item (Vector a) = a

Methods

fromList :: [Item (Vector a)] -> Vector a #

fromListN :: Int -> [Item (Vector a)] -> Vector a #

toList :: Vector a -> [Item (Vector a)] #

Storable a => IsList (Vector a) 
Instance details

Defined in Data.Vector.Storable

Associated Types

type Item (Vector a) 
Instance details

Defined in Data.Vector.Storable

type Item (Vector a) = a

Methods

fromList :: [Item (Vector a)] -> Vector a #

fromListN :: Int -> [Item (Vector a)] -> Vector a #

toList :: Vector a -> [Item (Vector a)] #

IsList [a] 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item [a] 
Instance details

Defined in GHC.Internal.IsList

type Item [a] = a

Methods

fromList :: [Item [a]] -> [a] #

fromListN :: Int -> [Item [a]] -> [a] #

toList :: [a] -> [Item [a]] #

Ord k => IsList (Map k v) 
Instance details

Defined in Data.Map.Internal

Associated Types

type Item (Map k v) 
Instance details

Defined in Data.Map.Internal

type Item (Map k v) = (k, v)

Methods

fromList :: [Item (Map k v)] -> Map k v #

fromListN :: Int -> [Item (Map k v)] -> Map k v #

toList :: Map k v -> [Item (Map k v)] #

(Eq k, Hashable k) => IsList (HashMap k v) 
Instance details

Defined in Data.HashMap.Internal

Associated Types

type Item (HashMap k v) 
Instance details

Defined in Data.HashMap.Internal

type Item (HashMap k v) = (k, v)

Methods

fromList :: [Item (HashMap k v)] -> HashMap k v #

fromListN :: Int -> [Item (HashMap k v)] -> HashMap k v #

toList :: HashMap k v -> [Item (HashMap k v)] #

type family Item l #

Instances

Instances details
type Item ByteArray 
Instance details

Defined in Data.Array.Byte

type Item ByteArray = Word8
type Item ByteString 
Instance details

Defined in Data.ByteString.Internal.Type

type Item ByteString = Word8
type Item ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

type Item ByteString = Word8
type Item ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

type Item ShortByteString = Word8
type Item IntSet 
Instance details

Defined in Data.IntSet.Internal

type Item IntSet = Key
type Item Version 
Instance details

Defined in GHC.Internal.IsList

type Item Version = Int
type Item CallStack 
Instance details

Defined in GHC.Internal.IsList

type Item CallStack = (String, SrcLoc)
type Item Text 
Instance details

Defined in Data.Text

type Item Text = Char
type Item Text 
Instance details

Defined in Data.Text.Lazy

type Item Text = Char
type Item ShortText 
Instance details

Defined in Data.Text.Short.Internal

type Item ShortText = Char
type Item (List2 a) Source # 
Instance details

Defined in Agda.Utils.List2

type Item (List2 a) = a
type Item (IntMap a) 
Instance details

Defined in Data.IntMap.Internal

type Item (IntMap a) = (Key, a)
type Item (Seq a) 
Instance details

Defined in Data.Sequence.Internal

type Item (Seq a) = a
type Item (Set a) 
Instance details

Defined in Data.Set.Internal

type Item (Set a) = a
type Item (DNonEmpty a) 
Instance details

Defined in Data.DList.DNonEmpty.Internal

type Item (DNonEmpty a) = a
type Item (DList a) 
Instance details

Defined in Data.DList.Internal

type Item (DList a) = a
type Item (NonEmpty a) 
Instance details

Defined in GHC.Internal.IsList

type Item (NonEmpty a) = a
type Item (ZipList a) 
Instance details

Defined in GHC.Internal.IsList

type Item (ZipList a) = a
type Item (HashSet a) 
Instance details

Defined in Data.HashSet.Internal

type Item (HashSet a) = a
type Item (Array a) 
Instance details

Defined in Data.Primitive.Array

type Item (Array a) = a
type Item (PrimArray a) 
Instance details

Defined in Data.Primitive.PrimArray

type Item (PrimArray a) = a
type Item (SmallArray a) 
Instance details

Defined in Data.Primitive.SmallArray

type Item (SmallArray a) = a
type Item (KeyMap v) 
Instance details

Defined in Data.Aeson.KeyMap

type Item (KeyMap v) = (Key, v)
type Item (Vector a) 
Instance details

Defined in Data.Vector

type Item (Vector a) = a
type Item (Vector a) 
Instance details

Defined in Data.Vector.Primitive

type Item (Vector a) = a
type Item (Vector a) 
Instance details

Defined in Data.Vector.Storable

type Item (Vector a) = a
type Item (Vector e) 
Instance details

Defined in Data.Vector.Unboxed

type Item (Vector e) = e
type Item [a] 
Instance details

Defined in GHC.Internal.IsList

type Item [a] = a
type Item (Map k v) 
Instance details

Defined in Data.Map.Internal

type Item (Map k v) = (k, v)
type Item (HashMap k v) 
Instance details

Defined in Data.HashMap.Internal

type Item (HashMap k v) = (k, v)

unzip :: Functor f => f (a, b) -> (f a, f b) #