Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Agda.Utils.Size
Description
Collection size.
For TermSize
see Agda.Syntax.Internal.
- class Sized a where
- data SizedThing a = SizedThing {
- theSize :: !Int
- sizedThing :: a
- sizeThing :: Sized a => a -> SizedThing a
Documentation
The size of a collection (i.e., its length).
Should fit into an Int
. TODO: change to Int
.
Minimal complete definition
Instances
Sized IntSet # | |
Sized Permutation # | |
Sized TopLevelModuleName # | |
Sized ModuleName # | |
Sized QName # | |
Sized [a] # | |
Sized (IntMap a) # | |
Sized (Seq a) # | |
Sized (Set a) # | |
Sized (HashSet 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) # | |
Sized (HashMap 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
|
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.