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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Size

Description

Collection size.

For TermSize see Agda.Syntax.Internal.

Synopsis

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 (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) 

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.