Agda.Utils.Size

Collection size.

For TermSize see Agda.Syntax.Internal.

Documentation

class Sized a where

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

Should fit into an Int. TODO: change to Int.

Minimal complete definition

size

Methods

size :: Integral n => a -> n

Instances

Sized IntSet

Methods

size :: Integral n => IntSet -> n

Sized Permutation

Methods

size :: Integral n => Permutation -> n

Sized TopLevelModuleName

Methods

size :: Integral n => TopLevelModuleName -> n

Sized ModuleName

Methods

size :: Integral n => ModuleName -> n

Sized QName

Methods

size :: Integral n => QName -> n

Sized [a]

Methods

size :: Integral n => [a] -> n

Sized (IntMap a)

Methods

size :: Integral n => IntMap a -> n

Sized (Seq a)

Methods

size :: Integral n => Seq a -> n

Sized (Set a)

Methods

size :: Integral n => Set a -> n

Sized (HashSet a)

Methods

size :: Integral n => HashSet a -> n

Sized (SizedThing a)

Return the cached size.

Methods

size :: Integral n => SizedThing a -> n

Sized (Tele a)

The size of a telescope is its length (as a list).

Methods

size :: Integral n => Tele a -> n

Sized a => Sized (Abs a)

Methods

size :: Integral n => Abs a -> n

Sized (Map k a)

Methods

size :: Integral n => Map k a -> n

Sized (HashMap k a)

Methods

size :: Integral n => HashMap k a -> n

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)

Methods

empty :: SizedThing a

null :: SizedThing a -> Bool

Sized (SizedThing a)

Return the cached size.

Methods

size :: Integral n => SizedThing a -> n

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

Cache the size of an object.