Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Minimal complete definition

Nothing

Methods

size :: a -> Int Source #

default size :: (Foldable t, t b ~ a) => a -> Int Source #

Instances

Instances details
Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Sized OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

size :: OccursWhere -> Int Source #

Sized Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Methods

size :: Permutation -> Int Source #

Sized IntSet Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: IntSet -> Int Source #

Sized a => Sized (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

Sized (Tele a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int Source #

Sized (List1 a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: List1 a -> Int Source #

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int Source #

Sized (IntMap a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: IntMap a -> Int Source #

Sized (Seq a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Seq a -> Int Source #

Sized (Set a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Set a -> Int Source #

Sized (HashSet a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashSet a -> Int Source #

Sized [a] Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: [a] -> Int Source #

Sized (Map k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Map k a -> Int Source #

Sized (HashMap k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashMap k a -> Int 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

Instances details
Null a => Null (SizedThing a) Source # 
Instance details

Defined in Agda.Utils.Size

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int Source #

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

Cache the size of an object.