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.

Methods

size :: Integral n => a -> n

Instances

Sized IntSet

Sized ModuleName

Sized QName

Sized Permutation

Sized [a]

Sized (IntMap a)

Sized (Set a)

Sized (Seq a)

Sized (HashSet a)

Sized (SizedThing a)

Return the cached size.

Sized (Tele a)

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

Sized a => Sized (Abs a)

Sized (Map k a)

Sized (HashMap k a)

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)

Sized (SizedThing a)

Return the cached size.

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

Cache the size of an object.