Agda.Utils.Singleton

Constructing singleton collections.

Documentation

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

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

Minimal complete definition

Nothing

Methods

fromList :: [el] -> coll

Instances

Collection Int IntSet

Defined in Agda.Utils.Singleton

Methods

fromList :: [Int] -> IntSet

SmallSetElement a => Collection a (SmallSet a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> SmallSet a

Collection a (Endo [a])

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> Endo [a]

Collection a (Seq a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> Seq a

Ord a => Collection a (Set a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> Set a

Collection a (DList a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> DList a

(Eq a, Hashable a) => Collection a (HashSet a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> HashSet a

Collection a [a]

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> [a]

Collection a ([a] -> [a])

Defined in Agda.Utils.Singleton

Methods

fromList :: [a] -> [a] -> [a]

Collection (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

fromList :: [Call cinfo] -> CallGraph cinfo

Collection (Int, a) (IntMap a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [(Int, a)] -> IntMap a

Ord k => Collection (k, a) (Map k a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [(k, a)] -> Map k a

(Eq k, Hashable k) => Collection (k, a) (HashMap k a)

Defined in Agda.Utils.Singleton

Methods

fromList :: [(k, a)] -> HashMap k a

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

Create-only collection with at most one element.

Minimal complete definition

Nothing

Methods

cMaybe :: Maybe el -> coll

Instances

CMaybe a (Maybe a)

Defined in Agda.Utils.Singleton

Methods

cMaybe :: Maybe a -> Maybe a

CMaybe a [a]

Defined in Agda.Utils.Singleton

Methods

cMaybe :: Maybe a -> [a]

class Singleton el coll | coll -> el where

Overloaded singleton constructor for collections.

Methods

singleton :: el -> coll

Instances

Singleton MetaId MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> MetaSet

Singleton MetaId ()

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> ()

Singleton Variable VarCounts

Defined in Agda.TypeChecking.Free

Methods

singleton :: Variable -> VarCounts

Singleton Int IntSet

Defined in Agda.Utils.Singleton

Methods

singleton :: Int -> IntSet

Singleton Variable (VarMap' a)

A "set"-style Singleton instance with default/initial variable occurrence.

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: Variable -> VarMap' a

Singleton a (Favorites a)

Defined in Agda.Utils.Favorites

Methods

singleton :: a -> Favorites a

SmallSetElement a => Singleton a (SmallSet a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> SmallSet a

Singleton a (Endo [a])

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> Endo [a]

Singleton a (NonEmpty a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> NonEmpty a

Singleton a (Seq a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> Seq a

Singleton a (Set a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> Set a

Singleton a (DList a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> DList a

Hashable a => Singleton a (HashSet a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> HashSet a

Singleton a (Maybe a)

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> Maybe a

Singleton a [a]

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> [a]

Singleton a ([a] -> [a])

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> [a] -> [a]

Singleton (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

singleton :: Call cinfo -> CallGraph cinfo

Singleton (CallMatrixAug cinfo) (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

singleton :: CallMatrixAug cinfo -> CMSet cinfo

Singleton (Variable, FlexRig' ()) FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: (Variable, FlexRig' ()) -> FlexRigMap

Singleton (Int, a) (IntMap a)

Defined in Agda.Utils.Singleton

Methods

singleton :: (Int, a) -> IntMap a

Singleton (k, a) (Map k a)

Defined in Agda.Utils.Singleton

Methods

singleton :: (k, a) -> Map k a

Hashable k => Singleton (k, a) (HashMap k a)

Defined in Agda.Utils.Singleton

Methods

singleton :: (k, a) -> HashMap k a