Safe Haskell	Safe-Inferred
Language	Haskell2010

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

type List1 = NonEmpty
type String1 = List1 Char
catMaybes :: List1 (Maybe a) -> [a]
mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
partitionEithers :: List1 (Either a b) -> ([a], [b])
zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
ifNull :: [a] -> b -> (List1 a -> b) -> b
union :: Eq a => List1 a -> List1 a -> List1 a
initLast :: List1 a -> ([a], a)
find :: (a -> Bool) -> List1 a -> Maybe a
lefts :: List1 (Either a b) -> [a]
snoc :: [a] -> a -> List1 a
updateHead :: (a -> a) -> List1 a -> List1 a
updateLast :: (a -> a) -> List1 a -> List1 a
concat :: [List1 a] -> [a]
foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
unwords :: List1 String -> String
rights :: List1 (Either a b) -> [b]
last2 :: List1 a -> Maybe (a, a)
ifNotNull :: [a] -> (List1 a -> b) -> b -> b
unlessNull :: Null m => [a] -> (List1 a -> m) -> m
breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
allEqual :: Eq a => List1 a -> Bool
nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
wordsBy :: (a -> Bool) -> [a] -> [List1 a]
toList' :: Maybe (List1 a) -> [a]
fromListSafe :: List1 a -> [a] -> List1 a
groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, List1 b)]
groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
data NonEmpty a = 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
length :: NonEmpty a -> Int
nonEmpty :: [a] -> Maybe (NonEmpty a)
transpose :: NonEmpty (NonEmpty a) -> NonEmpty (NonEmpty a)
tails :: Foldable f => f a -> NonEmpty [a]
unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b
unzip :: Functor f => f (a, b) -> (f a, f 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])
cycle :: NonEmpty a -> NonEmpty a
dropWhile :: (a -> Bool) -> NonEmpty a -> [a]
head :: NonEmpty a -> a
init :: NonEmpty a -> [a]
iterate :: (a -> a) -> a -> NonEmpty a
last :: NonEmpty a -> a
repeat :: a -> NonEmpty a
reverse :: NonEmpty 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]
zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c
cons :: a -> NonEmpty a -> NonEmpty a
uncons :: NonEmpty a -> (a, Maybe (NonEmpty a))
xor :: NonEmpty Bool -> Bool
intersperse :: a -> NonEmpty a -> 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
append :: NonEmpty a -> NonEmpty a -> NonEmpty a
tails1 :: NonEmpty a -> NonEmpty (NonEmpty a)
unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b
inits1 :: NonEmpty a -> NonEmpty (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)
groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [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)
sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a
class IsList l where
- type Item l
- fromList :: [Item l] -> l
- fromListN :: Int -> [Item l] -> l
- toList :: l -> [Item l]
type family Item l

Documentation

type List1 = NonEmpty Source #

type String1 = List1 Char Source #

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

Like catMaybes.

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

Like mapMaybe.

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 #

Like partitionEithers.

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

Like zipWithM.

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).

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.

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

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

unwords :: List1 String -> String Source #

Like unwords.

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 #

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' :: forall a. (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 :: forall a b. Eq a => [(a, b)] -> [(a, List1 b)] Source #

Group consecutive items that share the same first component.

groupByFst1 :: forall a b. 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).

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 #
MonadFix NonEmpty
Instance details Defined in Control.Monad.Fix Methods mfix :: (a -> NonEmpty a) -> NonEmpty a
Foldable NonEmpty
Instance details Defined in 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
Traversable NonEmpty
Instance details Defined in 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)
Applicative NonEmpty
Instance details Defined in GHC.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.Base Methods fmap :: (a -> b) -> NonEmpty a -> NonEmpty b (<$) :: a -> NonEmpty b -> NonEmpty a #
Monad NonEmpty
Instance details Defined in GHC.Base Methods (>>=) :: NonEmpty a -> (a -> NonEmpty b) -> NonEmpty b (>>) :: NonEmpty a -> NonEmpty b -> NonEmpty b return :: a -> NonEmpty a
NFData1 NonEmpty
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a -> ()) -> 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.Generics Associated Types type Rep1 NonEmpty :: k -> Type Methods from1 :: forall (a :: k). NonEmpty a -> Rep1 NonEmpty a to1 :: forall (a :: k). 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 Methods recurseExpr :: RecurseExprFn m (List1 a) Source # foldExpr :: FoldExprFn m (List1 a) Source # traverseExpr :: TraverseExprFn m (List1 a) Source # mapExpr :: (Expr -> Expr) -> List1 a -> List1 a Source #
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 Methods killRange :: KillRangeT (List1 a) Source #
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) Source # Methods toConcrete :: List1 a -> AbsToCon (ConOfAbs (List1 a)) Source # bindToConcrete :: List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (List1 c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (List1 c) Source # Methods toAbstract :: List1 c -> ScopeM (AbsOfCon (List1 c)) Source #
ToAbstract (List1 (QNamed Clause)) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (List1 (QNamed Clause)) Source # Methods toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause))) Source #
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 #
Semigroup (NonEmpty a)
Instance details Defined in GHC.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.Generics Associated Types type Rep (NonEmpty a) :: Type -> Type Methods from :: NonEmpty a -> Rep (NonEmpty a) x to :: Rep (NonEmpty a) x -> NonEmpty a
IsList (NonEmpty a)
Instance details Defined in GHC.IsList Associated Types type Item (NonEmpty 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.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.Show Methods showsPrec :: Int -> NonEmpty a -> ShowS show :: NonEmpty a -> String showList :: [NonEmpty a] -> ShowS
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 -> ()
Eq a => Eq (NonEmpty a)
Instance details Defined in GHC.Base Methods (==) :: NonEmpty a -> NonEmpty a -> Bool (/=) :: NonEmpty a -> NonEmpty a -> Bool
Ord a => Ord (NonEmpty a)
Instance details Defined in GHC.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 Methods toJSON :: NonEmpty a -> Value # toEncoding :: NonEmpty a -> Encoding # toJSONList :: [NonEmpty a] -> Value # toEncodingList :: [NonEmpty a] -> Encoding # omitField :: NonEmpty a -> Bool #
AddContext (List1 Name, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
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 Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
type Rep1 NonEmpty
Instance details Defined in GHC.Generics type Rep1 NonEmpty = D1 ('MetaData "NonEmpty" "GHC.Base" "base" '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 List)))
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 AbsOfRef (List1 (QNamed Clause)) = List1 Clause
type Rep (NonEmpty a)
Instance details Defined in GHC.Generics type Rep (NonEmpty a) = D1 ('MetaData "NonEmpty" "GHC.Base" "base" '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.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 #

length :: NonEmpty a -> Int #

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

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

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

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

unzip :: Functor f => f (a, b) -> (f a, f 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]) #

cycle :: NonEmpty a -> NonEmpty a #

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

head :: NonEmpty a -> a #

init :: NonEmpty a -> [a] #

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

last :: NonEmpty a -> a #

repeat :: a -> NonEmpty a #

reverse :: NonEmpty 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] #

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

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

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

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

xor :: NonEmpty Bool -> Bool #

intersperse :: a -> NonEmpty a -> 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 #

append :: NonEmpty a -> NonEmpty a -> NonEmpty a #

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

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

inits1 :: NonEmpty a -> NonEmpty (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) #

groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [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) #

sortWith :: Ord o => (a -> o) -> NonEmpty a -> 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 # Methods fromList :: [Item ByteArray] -> ByteArray # fromListN :: Int -> [Item ByteArray] -> ByteArray # toList :: ByteArray -> [Item ByteArray] #
IsList Version
Instance details Defined in GHC.IsList Associated Types type Item Version # Methods fromList :: [Item Version] -> Version # fromListN :: Int -> [Item Version] -> Version # toList :: Version -> [Item Version] #
IsList CallStack
Instance details Defined in GHC.IsList Associated Types type Item CallStack # Methods fromList :: [Item CallStack] -> CallStack # fromListN :: Int -> [Item CallStack] -> CallStack # toList :: CallStack -> [Item CallStack] #
IsList ByteString
Instance details Defined in Data.ByteString.Internal.Type Associated Types type Item ByteString # 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 # 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 # 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 # Methods fromList :: [Item IntSet] -> IntSet # fromListN :: Int -> [Item IntSet] -> IntSet # toList :: IntSet -> [Item IntSet] #
IsList ShortText
Instance details Defined in Data.Text.Short.Internal Associated Types type Item ShortText # 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) # Methods fromList :: [Item (List2 a)] -> List2 a # fromListN :: Int -> [Item (List2 a)] -> List2 a # toList :: List2 a -> [Item (List2 a)] #
IsList (ZipList a)
Instance details Defined in GHC.IsList Associated Types type Item (ZipList a) # Methods fromList :: [Item (ZipList a)] -> ZipList a # fromListN :: Int -> [Item (ZipList a)] -> ZipList a # toList :: ZipList a -> [Item (ZipList a)] #
IsList (NonEmpty a)
Instance details Defined in GHC.IsList Associated Types type Item (NonEmpty a) # Methods fromList :: [Item (NonEmpty a)] -> NonEmpty a # fromListN :: Int -> [Item (NonEmpty a)] -> NonEmpty a # toList :: NonEmpty a -> [Item (NonEmpty a)] #
IsList (IntMap a)
Instance details Defined in Data.IntMap.Internal Associated Types type Item (IntMap 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) # 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) # 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) # 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) # Methods fromList :: [Item (DList a)] -> DList a # fromListN :: Int -> [Item (DList a)] -> DList a # toList :: DList a -> [Item (DList a)] #
(Eq a, Hashable a) => IsList (HashSet a)
Instance details Defined in Data.HashSet.Internal Associated Types type Item (HashSet 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) # 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) # 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) # 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) # 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) # 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) # 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) # 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.IsList Associated Types type Item [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) # 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) # 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 Version
Instance details Defined in GHC.IsList type Item Version = Int
type Item CallStack
Instance details Defined in GHC.IsList type Item CallStack = (String, SrcLoc)
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 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 (ZipList a)
Instance details Defined in GHC.IsList type Item (ZipList a) = a
type Item (NonEmpty a)
Instance details Defined in GHC.IsList type Item (NonEmpty 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 (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.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)