Agda.Utils.Size

Documentation

class Sized a where

The size of an object.

For collections, it returns the length of the collection, not the overall size including the elements.

Methods

size :: Integral n => a -> n

Instances

Sized IntSet

Sized Permutation

Sized ModuleName

Sized QName

Sized Substitution

Sized LevelAtom

Sized PlusLevel

Sized Level

Sized Type

Sized Term

Sized [a]

Sized (IntMap a)

Sized (Set a)

Sized (Seq a)

Sized (SizedThing a)

Return the cached size.

Sized (Tele a)

Sized a => Sized (Abs a)

Sized a => Sized (Elim' a)

Sized (Map k a)

Sized a => Sized (Named name a)

Sized a => Sized (Dom c a)

Sized a => Sized (Arg c 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.