Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.Size

Description

Collection size.

For TermSize see Agda.Syntax.Internal.

Synopsis

class Sized a where
data SizedThing a = SizedThing {
- theSize :: !Int
- sizedThing :: a
}
sizeThing :: Sized a => a -> SizedThing a

Documentation

class Sized a where #

The size of a collection (i.e., its length).

Minimal complete definition

size

Methods

size :: a -> Int #

Instances

Sized IntSet #
Instance details Defined in Agda.Utils.Size Methods size :: IntSet -> Int #
Sized Permutation #
Instance details Defined in Agda.Utils.Permutation Methods size :: Permutation -> Int #
Sized TopLevelModuleName #
Instance details Defined in Agda.Syntax.Concrete.Name Methods size :: TopLevelModuleName -> Int #
Sized ModuleName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: ModuleName -> Int #
Sized QName #
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: QName -> Int #
Sized OccursWhere #
Instance details Defined in Agda.TypeChecking.Positivity Methods size :: OccursWhere -> Int #
Sized [a] #
Instance details Defined in Agda.Utils.Size Methods size :: [a] -> Int #
Sized (IntMap a) #
Instance details Defined in Agda.Utils.Size Methods size :: IntMap a -> Int #
Sized (Seq a) #
Instance details Defined in Agda.Utils.Size Methods size :: Seq a -> Int #
Sized (Set a) #
Instance details Defined in Agda.Utils.Size Methods size :: Set a -> Int #
Sized (HashSet a) #
Instance details Defined in Agda.Utils.Size Methods size :: HashSet a -> Int #
Sized (SizedThing a) #	Return the cached size.
Instance details Defined in Agda.Utils.Size Methods size :: SizedThing a -> Int #
Sized (Tele a) #	The size of a telescope is its length (as a list).
Instance details Defined in Agda.Syntax.Internal Methods size :: Tele a -> Int #
Sized a => Sized (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods size :: Abs a -> Int #
Sized (Map k a) #
Instance details Defined in Agda.Utils.Size Methods size :: Map k a -> Int #
Sized (HashMap k a) #
Instance details Defined in Agda.Utils.Size Methods size :: HashMap k a -> Int #

data SizedThing a #

Thing decorated with its size. The thing should fit into main memory, thus, the size is an Int.

Constructors

SizedThing
Fields theSize :: !Int sizedThing :: a

Instances

Null a => Null (SizedThing a) #
Instance details Defined in Agda.Utils.Size Methods empty :: SizedThing a # null :: SizedThing a -> Bool #
Sized (SizedThing a) #	Return the cached size.
Instance details Defined in Agda.Utils.Size Methods size :: SizedThing a -> Int #

sizeThing :: Sized a => a -> SizedThing a #

Cache the size of an object.