Safe Haskell	None
Language	Haskell2010

Agda.Utils.Set1

Description

Non-empty sets.

Provides type Set1 of non-empty sets.

Import: @

import Agda.Utils.Set1 (Set1) import qualified Agda.Utils.Set1 as Set1

@

Synopsis

ifNull :: Set a -> b -> (Set1 a -> b) -> b
toSet' :: Maybe (Set1 a) -> Set a
unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m ()
unlessNullM :: Monad m => m (Set a) -> (Set1 a -> m ()) -> m ()
type Set1 = NESet
pattern IsEmpty :: Set a
pattern IsNonEmpty :: NESet a -> Set a
(\\) :: Ord a => NESet a -> NESet a -> Set a
cartesianProduct :: NESet a -> NESet b -> NESet (a, b)
delete :: Ord a => a -> NESet a -> Set a
deleteAt :: Int -> NESet a -> Set a
deleteFindMax :: NESet a -> (a, Set a)
deleteFindMin :: NESet a -> (a, Set a)
deleteMax :: NESet a -> Set a
deleteMin :: NESet a -> Set a
difference :: Ord a => NESet a -> NESet a -> Set a
disjoint :: Ord a => NESet a -> NESet a -> Bool
disjointUnion :: NESet a -> NESet b -> NESet (Either a b)
drop :: Int -> NESet a -> Set a
dropWhileAntitone :: (a -> Bool) -> NESet a -> Set a
elemAt :: Int -> NESet a -> a
elems :: NESet a -> NonEmpty a
filter :: (a -> Bool) -> NESet a -> Set a
findIndex :: Ord a => a -> NESet a -> Int
findMax :: NESet a -> a
findMin :: NESet a -> a
foldl1' :: (a -> a -> a) -> NESet a -> a
foldr1' :: (a -> a -> a) -> NESet a -> a
fromAscList :: Eq a => NonEmpty a -> NESet a
fromDescList :: Eq a => NonEmpty a -> NESet a
fromDistinctAscList :: NonEmpty a -> NESet a
fromDistinctDescList :: NonEmpty a -> NESet a
insert :: Ord a => a -> NESet a -> NESet a
insertSet :: Ord a => a -> Set a -> NESet a
insertSetMax :: a -> Set a -> NESet a
insertSetMin :: a -> Set a -> NESet a
intersection :: Ord a => NESet a -> NESet a -> Set a
isProperSubsetOf :: Ord a => NESet a -> NESet a -> Bool
isSubsetOf :: Ord a => NESet a -> NESet a -> Bool
lookupGE :: Ord a => a -> NESet a -> Maybe a
lookupGT :: Ord a => a -> NESet a -> Maybe a
lookupIndex :: Ord a => a -> NESet a -> Maybe Int
lookupLE :: Ord a => a -> NESet a -> Maybe a
lookupLT :: Ord a => a -> NESet a -> Maybe a
map :: Ord b => (a -> b) -> NESet a -> NESet b
mapMonotonic :: (a -> b) -> NESet a -> NESet b
member :: Ord a => a -> NESet a -> Bool
notMember :: Ord a => a -> NESet a -> Bool
partition :: (a -> Bool) -> NESet a -> These (NESet a) (NESet a)
powerSet :: NESet a -> NESet (NESet a)
spanAntitone :: (a -> Bool) -> NESet a -> These (NESet a) (NESet a)
split :: Ord a => a -> NESet a -> Maybe (These (NESet a) (NESet a))
splitAt :: Int -> NESet a -> These (NESet a) (NESet a)
splitMember :: Ord a => a -> NESet a -> (Bool, Maybe (These (NESet a) (NESet a)))
splitRoot :: NESet a -> NonEmpty (NESet a)
take :: Int -> NESet a -> Set a
takeWhileAntitone :: (a -> Bool) -> NESet a -> Set a
toAscList :: NESet a -> NonEmpty a
toDescList :: NESet a -> NonEmpty a
unsafeFromSet :: Set a -> NESet a
foldl :: (a -> b -> a) -> a -> NESet b -> a
foldl' :: (a -> b -> a) -> a -> NESet b -> a
foldr :: (a -> b -> b) -> b -> NESet a -> b
foldr' :: (a -> b -> b) -> b -> NESet a -> b
fromList :: Ord a => NonEmpty a -> NESet a
nonEmptySet :: Set a -> Maybe (NESet a)
singleton :: a -> NESet a
size :: NESet a -> Int
toList :: NESet a -> NonEmpty a
toSet :: NESet a -> Set a
union :: Ord a => NESet a -> NESet a -> NESet a
unions :: (Foldable1 f, Ord a) => f (NESet a) -> NESet a
valid :: Ord a => NESet a -> Bool
withNonEmpty :: r -> (NESet a -> r) -> Set a -> r
foldl1 :: Foldable t => (a -> a -> a) -> t a -> a
foldr1 :: Foldable t => (a -> a -> a) -> t a -> a
data NESet a

Documentation

ifNull :: Set a -> b -> (Set1 a -> b) -> b Source #

toSet' :: Maybe (Set1 a) -> Set a Source #

Lossless toSet. Opposite of nonEmptySet.

unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m () Source #

A more general type would be Null m => Set a -> (Set1 a -> m) -> m but this type is problematic as we do not have a general instance Applicative m => Null (m ()).

unlessNullM :: Monad m => m (Set a) -> (Set1 a -> m ()) -> m () Source #

type Set1 = NESet Source #

pattern IsEmpty :: Set a #

pattern IsNonEmpty :: NESet a -> Set a #

(\\) :: Ord a => NESet a -> NESet a -> Set a #

cartesianProduct :: NESet a -> NESet b -> NESet (a, b) #

delete :: Ord a => a -> NESet a -> Set a #

deleteAt :: Int -> NESet a -> Set a #

deleteFindMax :: NESet a -> (a, Set a) #

deleteFindMin :: NESet a -> (a, Set a) #

deleteMax :: NESet a -> Set a #

deleteMin :: NESet a -> Set a #

difference :: Ord a => NESet a -> NESet a -> Set a #

disjoint :: Ord a => NESet a -> NESet a -> Bool #

disjointUnion :: NESet a -> NESet b -> NESet (Either a b) #

drop :: Int -> NESet a -> Set a #

dropWhileAntitone :: (a -> Bool) -> NESet a -> Set a #

elemAt :: Int -> NESet a -> a #

elems :: NESet a -> NonEmpty a #

filter :: (a -> Bool) -> NESet a -> Set a #

findIndex :: Ord a => a -> NESet a -> Int #

findMax :: NESet a -> a #

findMin :: NESet a -> a #

foldl1' :: (a -> a -> a) -> NESet a -> a #

foldr1' :: (a -> a -> a) -> NESet a -> a #

fromAscList :: Eq a => NonEmpty a -> NESet a #

fromDescList :: Eq a => NonEmpty a -> NESet a #

fromDistinctAscList :: NonEmpty a -> NESet a #

fromDistinctDescList :: NonEmpty a -> NESet a #

insert :: Ord a => a -> NESet a -> NESet a #

insertSet :: Ord a => a -> Set a -> NESet a #

insertSetMax :: a -> Set a -> NESet a #

insertSetMin :: a -> Set a -> NESet a #

intersection :: Ord a => NESet a -> NESet a -> Set a #

isProperSubsetOf :: Ord a => NESet a -> NESet a -> Bool #

isSubsetOf :: Ord a => NESet a -> NESet a -> Bool #

lookupGE :: Ord a => a -> NESet a -> Maybe a #

lookupGT :: Ord a => a -> NESet a -> Maybe a #

lookupIndex :: Ord a => a -> NESet a -> Maybe Int #

lookupLE :: Ord a => a -> NESet a -> Maybe a #

lookupLT :: Ord a => a -> NESet a -> Maybe a #

map :: Ord b => (a -> b) -> NESet a -> NESet b #

mapMonotonic :: (a -> b) -> NESet a -> NESet b #

member :: Ord a => a -> NESet a -> Bool #

notMember :: Ord a => a -> NESet a -> Bool #

partition :: (a -> Bool) -> NESet a -> These (NESet a) (NESet a) #

powerSet :: NESet a -> NESet (NESet a) #

spanAntitone :: (a -> Bool) -> NESet a -> These (NESet a) (NESet a) #

split :: Ord a => a -> NESet a -> Maybe (These (NESet a) (NESet a)) #

splitAt :: Int -> NESet a -> These (NESet a) (NESet a) #

splitMember :: Ord a => a -> NESet a -> (Bool, Maybe (These (NESet a) (NESet a))) #

splitRoot :: NESet a -> NonEmpty (NESet a) #

take :: Int -> NESet a -> Set a #

takeWhileAntitone :: (a -> Bool) -> NESet a -> Set a #

toAscList :: NESet a -> NonEmpty a #

toDescList :: NESet a -> NonEmpty a #

unsafeFromSet :: Set a -> NESet a #

foldl :: (a -> b -> a) -> a -> NESet b -> a #

foldl' :: (a -> b -> a) -> a -> NESet b -> a #

foldr :: (a -> b -> b) -> b -> NESet a -> b #

foldr' :: (a -> b -> b) -> b -> NESet a -> b #

fromList :: Ord a => NonEmpty a -> NESet a #

nonEmptySet :: Set a -> Maybe (NESet a) #

singleton :: a -> NESet a #

size :: NESet a -> Int #

toList :: NESet a -> NonEmpty a #

toSet :: NESet a -> Set a #

union :: Ord a => NESet a -> NESet a -> NESet a #

unions :: (Foldable1 f, Ord a) => f (NESet a) -> NESet a #

valid :: Ord a => NESet a -> Bool #

withNonEmpty :: r -> (NESet a -> r) -> Set a -> r #

foldl1 :: Foldable t => (a -> a -> a) -> t a -> a #

A variant of foldl that has no base case, and thus may only be applied to non-empty structures.

This function is non-total and will raise a runtime exception if the structure happens to be empty.

foldl1 f = foldl1 f . toList

Examples

Expand

Basic usage:

>>> foldl1 (+) [1..4]
10

>>> foldl1 (+) []
*** Exception: Prelude.foldl1: empty list

>>> foldl1 (+) Nothing
*** Exception: foldl1: empty structure

>>> foldl1 (-) [1..4]
-8

>>> foldl1 (&&) [True, False, True, True]
False

>>> foldl1 (||) [False, False, True, True]
True

>>> foldl1 (+) [1..]
* Hangs forever *

foldr1 :: Foldable t => (a -> a -> a) -> t a -> a #

A variant of foldr that has no base case, and thus may only be applied to non-empty structures.

This function is non-total and will raise a runtime exception if the structure happens to be empty.

Examples

Expand

Basic usage:

>>> foldr1 (+) [1..4]
10

>>> foldr1 (+) []
Exception: Prelude.foldr1: empty list

>>> foldr1 (+) Nothing
*** Exception: foldr1: empty structure

>>> foldr1 (-) [1..4]
-2

>>> foldr1 (&&) [True, False, True, True]
False

>>> foldr1 (||) [False, False, True, True]
True

>>> foldr1 (+) [1..]
* Hangs forever *

data NESet a #

Instances

Instances details

Foldable1 NESet #
Instance details Defined in Data.Set.NonEmpty.Internal Methods fold1 :: Semigroup m => NESet m -> m # foldMap1 :: Semigroup m => (a -> m) -> NESet a -> m # foldMap1' :: Semigroup m => (a -> m) -> NESet a -> m # toNonEmpty :: NESet a -> NonEmpty a # maximum :: Ord a => NESet a -> a # minimum :: Ord a => NESet a -> a # head :: NESet a -> a # last :: NESet a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> NESet a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> NESet a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> NESet a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> NESet a -> b #
Eq1 NESet #
Instance details Defined in Data.Set.NonEmpty.Internal Methods liftEq :: (a -> b -> Bool) -> NESet a -> NESet b -> Bool #
Ord1 NESet #
Instance details Defined in Data.Set.NonEmpty.Internal Methods liftCompare :: (a -> b -> Ordering) -> NESet a -> NESet b -> Ordering #
Show1 NESet #
Instance details Defined in Data.Set.NonEmpty.Internal Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> NESet a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [NESet a] -> ShowS #
Foldable NESet #
Instance details Defined in Data.Set.NonEmpty.Internal Methods fold :: Monoid m => NESet m -> m # foldMap :: Monoid m => (a -> m) -> NESet a -> m # foldMap' :: Monoid m => (a -> m) -> NESet a -> m # foldr :: (a -> b -> b) -> b -> NESet a -> b # foldr' :: (a -> b -> b) -> b -> NESet a -> b # foldl :: (b -> a -> b) -> b -> NESet a -> b # foldl' :: (b -> a -> b) -> b -> NESet a -> b # foldr1 :: (a -> a -> a) -> NESet a -> a # foldl1 :: (a -> a -> a) -> NESet a -> a # toList :: NESet a -> [a] # null :: NESet a -> Bool # length :: NESet a -> Int # elem :: Eq a => a -> NESet a -> Bool # maximum :: Ord a => NESet a -> a # minimum :: Ord a => NESet a -> a # sum :: Num a => NESet a -> a # product :: Num a => NESet a -> a #
Singleton a (NESet a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> NESet a Source #
HasRange a => HasRange (Set1 a) Source #
Instance details Defined in Agda.Syntax.Position Methods getRange :: Set1 a -> Range Source #
HasRangeWithoutFile a => HasRangeWithoutFile (Set1 a) Source #
Instance details Defined in Agda.Syntax.Position Methods getRangeWithoutFile :: Set1 a -> RangeWithoutFile Source #
(Ord a, KillRange a) => KillRange (Set1 a) Source #
Instance details Defined in Agda.Syntax.Position Methods killRange :: KillRangeT (Set1 a) Source #
(Ord a, EmbPrj a) => EmbPrj (Set1 a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Set1 a -> S Word32 Source # icod_ :: Set1 a -> S Word32 Source # value :: Word32 -> R (Set1 a) Source #
NFData a => NFData (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods rnf :: NESet a -> () #
Ord a => Semigroup (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods (<>) :: NESet a -> NESet a -> NESet a # sconcat :: NonEmpty (NESet a) -> NESet a # stimes :: Integral b => b -> NESet a -> NESet a #
(Data a, Ord a) => Data (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NESet a -> c (NESet a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NESet a) # toConstr :: NESet a -> Constr # dataTypeOf :: NESet a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NESet a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NESet a)) # gmapT :: (forall b. Data b => b -> b) -> NESet a -> NESet a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NESet a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NESet a -> r # gmapQ :: (forall d. Data d => d -> u) -> NESet a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NESet a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NESet a -> m (NESet a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NESet a -> m (NESet a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NESet a -> m (NESet a) #
(Read a, Ord a) => Read (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods readsPrec :: Int -> ReadS (NESet a) # readList :: ReadS [NESet a] # readPrec :: ReadPrec (NESet a) # readListPrec :: ReadPrec [NESet a] #
Show a => Show (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods showsPrec :: Int -> NESet a -> ShowS # show :: NESet a -> String # showList :: [NESet a] -> ShowS #
Eq a => Eq (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods (==) :: NESet a -> NESet a -> Bool # (/=) :: NESet a -> NESet a -> Bool #
Ord a => Ord (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods compare :: NESet a -> NESet a -> Ordering # (<) :: NESet a -> NESet a -> Bool # (<=) :: NESet a -> NESet a -> Bool # (>) :: NESet a -> NESet a -> Bool # (>=) :: NESet a -> NESet a -> Bool # max :: NESet a -> NESet a -> NESet a # min :: NESet a -> NESet a -> NESet a #
(FromJSON a, Ord a) => FromJSON (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods parseJSON :: Value -> Parser (NESet a) # parseJSONList :: Value -> Parser [NESet a] # omittedField :: Maybe (NESet a) #
ToJSON a => ToJSON (NESet a) #
Instance details Defined in Data.Set.NonEmpty.Internal Methods toJSON :: NESet a -> Value # toEncoding :: NESet a -> Encoding # toJSONList :: [NESet a] -> Value # toEncodingList :: [NESet a] -> Encoding # omitField :: NESet a -> Bool #