Safe Haskell	None
Language	Haskell2010

Agda.Utils.Singleton

Description

Constructing singleton collections.

Synopsis

class (Semigroup coll, Monoid coll, Singleton el coll) => Collection el coll | coll -> el where
- fromList :: [el] -> coll
class (Null coll, Singleton el coll) => CMaybe el coll | coll -> el where
- cMaybe :: Maybe el -> coll
class Singleton el coll | coll -> el where
- singleton :: el -> coll

Documentation

class (Semigroup coll, Monoid coll, Singleton el coll) => Collection el coll | coll -> el where Source #

A create-only possibly empty collection is a monoid with the possibility to inject elements.

Minimal complete definition

Nothing

Methods

fromList :: [el] -> coll Source #

Instances

Instances details

Collection Int IntSet Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [Int] -> IntSet Source #
Collection a (Seq a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [a] -> Seq a Source #
Collection a (DList a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [a] -> DList a Source #
Collection a (Endo [a]) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [a] -> Endo [a] Source #
Collection a [a] Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [a] -> [a] Source #
SmallSetElement k => Collection k (SmallSet k) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [k] -> SmallSet k Source #
Ord k => Collection k (Set k) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [k] -> Set k Source #
Enum k => Collection k (EnumSet k) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [k] -> EnumSet k Source #
(Eq k, Hashable k) => Collection k (HashSet k) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [k] -> HashSet k Source #
Collection a ([a] -> [a]) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [a] -> [a] -> [a] Source #
Collection (Call cinfo) (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods fromList :: [Call cinfo] -> CallGraph cinfo Source #
Collection (Int, a) (IntMap a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [(Int, a)] -> IntMap a Source #
Ord k => Collection (k, a) (Map k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [(k, a)] -> Map k a Source #
Enum k => Collection (k, a) (EnumMap k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [(k, a)] -> EnumMap k a Source #
(Eq k, Hashable k) => Collection (k, a) (HashMap k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods fromList :: [(k, a)] -> HashMap k a Source #

class (Null coll, Singleton el coll) => CMaybe el coll | coll -> el where Source #

Create-only collection with at most one element.

Minimal complete definition

Nothing

Methods

cMaybe :: Maybe el -> coll Source #

Instances

Instances details

CMaybe a (Maybe a) Source #
Instance details Defined in Agda.Utils.Singleton Methods cMaybe :: Maybe a -> Maybe a Source #
CMaybe a [a] Source #
Instance details Defined in Agda.Utils.Singleton Methods cMaybe :: Maybe a -> [a] Source #

class Singleton el coll | coll -> el where Source #

Overloaded singleton constructor for collections.

Methods

singleton :: el -> coll Source #

Instances

Instances details

Singleton MetaId MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> MetaSet Source #
Singleton MetaId () Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> () Source #
Singleton Variable VarCounts Source #
Instance details Defined in Agda.TypeChecking.Free Methods singleton :: Variable -> VarCounts Source #
Singleton Int VarSet Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: Int -> VarSet Source #
Singleton Int IntSet Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: Int -> IntSet Source #
Singleton Variable (VarMap' a) Source #	A "set"-style `Singleton` instance with default/initial variable occurrence.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: Variable -> VarMap' a Source #
Singleton a (Favorites a) Source #
Instance details Defined in Agda.Utils.Favorites Methods singleton :: a -> Favorites a Source #
SmallSetElement a => Singleton a (SmallSet a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> SmallSet a Source #
Singleton a (Seq a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> Seq a Source #
Singleton a (Set a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> Set a Source #
Singleton a (DList a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> DList a Source #
Enum a => Singleton a (EnumSet a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> EnumSet a Source #
Singleton a (NonEmpty a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> NonEmpty a Source #
Singleton a (Endo [a]) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> Endo [a] Source #
Singleton a (NESet a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> NESet a Source #
Singleton a (Maybe a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> Maybe a Source #
Singleton a [a] Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> [a] Source #
Hashable k => Singleton k (HashSet k) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: k -> HashSet k Source #
Singleton a ([a] -> [a]) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: a -> [a] -> [a] Source #
Singleton (Call cinfo) (CallGraph cinfo) Source #
Instance details Defined in Agda.Termination.CallGraph Methods singleton :: Call cinfo -> CallGraph cinfo Source #
Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source #
Instance details Defined in Agda.Termination.CallMatrix Methods singleton :: CallMatrixAug cinfo -> CMSet cinfo Source #
Singleton (Variable, FlexRig' ()) FlexRigMap Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, FlexRig' ()) -> FlexRigMap Source #
Singleton (Int, a) (IntMap a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: (Int, a) -> IntMap a Source #
Singleton ([k], v) (Trie k v) Source #
Instance details Defined in Agda.Utils.CompressedTrie Methods singleton :: ([k], v) -> Trie k v Source #
Singleton (k, a) (Map k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: (k, a) -> Map k a Source #
Enum k => Singleton (k, a) (EnumMap k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: (k, a) -> EnumMap k a Source #
Hashable k => Singleton (k, a) (HashMap k a) Source #
Instance details Defined in Agda.Utils.Singleton Methods singleton :: (k, a) -> HashMap k a Source #