| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Size
Description
Collection size.
For TermSize see Agda.Syntax.Internal.
Synopsis
- 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).
Instances
| Sized IntSet Source # | |
| Sized Permutation Source # | |
Defined in Agda.Utils.Permutation Methods size :: Permutation -> Int Source # | |
| Sized TopLevelModuleName Source # | |
Defined in Agda.Syntax.Concrete.Name Methods size :: TopLevelModuleName -> Int Source # | |
| Sized ModuleName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods size :: ModuleName -> Int Source # | |
| Sized QName Source # | |
| Sized OccursWhere Source # | |
Defined in Agda.TypeChecking.Positivity.Occurrence Methods size :: OccursWhere -> Int Source # | |
| Sized [a] Source # | |
Defined in Agda.Utils.Size | |
| Sized (IntMap a) Source # | |
| Sized (Seq a) Source # | |
| Sized (Set a) Source # | |
| Sized (HashSet a) Source # | |
Defined in Agda.Utils.Size | |
| Sized (SizedThing a) Source # | Return the cached size. |
Defined in Agda.Utils.Size Methods size :: SizedThing a -> Int Source # | |
| Sized (Tele a) Source # | The size of a telescope is its length (as a list). |
| Sized a => Sized (Abs a) Source # | |
| Sized (Map k a) Source # | |
| Sized (HashMap k a) Source # | |
Defined in Agda.Utils.Size | |
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 # | |
Defined in Agda.Utils.Size | |
| Sized (SizedThing a) Source # | Return the cached size. |
Defined in Agda.Utils.Size Methods size :: SizedThing a -> Int Source # | |
sizeThing :: Sized a => a -> SizedThing a Source #
Cache the size of an object.