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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Size

Description

Collection size.

For `TermSize` see Agda.Syntax.Internal.

Synopsis

- class Sized a where
  - size :: a -> Int
- data SizedThing a = SizedThing {
  - theSize :: !Int
  - sizedThing :: a
  }
- sizeThing :: Sized a => a -> SizedThing a

# 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 Methods size :: TopLevelModuleName -> Int Source #
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

- theSize :: !Int
- sizedThing :: a

#### Instances

Instances details

Null a => Null (SizedThing a) Source # |
Instance details Defined in Agda.Utils.Size Methods empty :: SizedThing a Source # null :: SizedThing a -> Bool Source #
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.