Agda-2.4.2.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Size

Synopsis

Documentation

class Sized a where Source

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 Source

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 Source

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 Source

Cache the size of an object.