Agda-2.5.1.2: 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 Source #

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 Source #

Instances

Sized IntSet Source # 

Methods

size :: Integral n => IntSet -> n Source #

Sized Permutation Source # 

Methods

size :: Integral n => Permutation -> n Source #

Sized ModuleName Source # 

Methods

size :: Integral n => ModuleName -> n Source #

Sized QName Source # 

Methods

size :: Integral n => QName -> n Source #

Sized OccursWhere Source # 

Methods

size :: Integral n => OccursWhere -> n Source #

Sized [a] Source # 

Methods

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

Sized (IntMap a) Source # 

Methods

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

Sized (Seq a) Source # 

Methods

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

Sized (Set a) Source # 

Methods

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

Sized (HashSet a) Source # 

Methods

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

Sized (SizedThing a) Source #

Return the cached size.

Methods

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

Sized (Tele a) Source #

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

Methods

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

Sized a => Sized (Abs a) Source # 

Methods

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

Sized (Map k a) Source # 

Methods

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

Sized (HashMap k a) Source # 

Methods

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

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

Instances

Null a => Null (SizedThing a) Source # 
Sized (SizedThing a) Source #

Return the cached size.

Methods

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

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

Cache the size of an object.