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

Safe HaskellSafe
LanguageHaskell2010

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.

Minimal complete definition

size

Methods

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

Instances

Sized IntSet # 

Methods

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

Sized Permutation # 

Methods

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

Sized TopLevelModuleName # 

Methods

size :: Integral n => TopLevelModuleName -> n #

Sized ModuleName # 

Methods

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

Sized QName # 

Methods

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

Sized [a] # 

Methods

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

Sized (IntMap a) # 

Methods

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

Sized (Seq a) # 

Methods

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

Sized (Set a) # 

Methods

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

Sized (HashSet a) # 

Methods

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

Sized (SizedThing a) #

Return the cached size.

Methods

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

Sized (Tele a) #

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

Methods

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

Sized a => Sized (Abs a) # 

Methods

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

Sized (Map k a) # 

Methods

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

Sized (HashMap k a) # 

Methods

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

data SizedThing a #

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

Methods

empty :: SizedThing a #

null :: SizedThing a -> Bool #

Sized (SizedThing a) #

Return the cached size.

Methods

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

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

Cache the size of an object.