Agda.Utils.Size · Agda-2.7.0.1

classclass Sized a where

The size of a collection (i.e., its length).

size :: a -> Int
Strict size computation.
Anti-patterns: size xs == n where n is 0, 1 or another number that is likely smaller than size xs. Similar for size xs >= 1 etc. Use natSize instead.
See https://wiki.haskell.org/Haskell_programming_tips#Don.27t_ask_for_the_length_of_a_list_when_you_don.27t_need_it .
natSize :: a -> Peano
Lazily compute a (possibly infinite) size.
Use when comparing a size against a fixed number.

Instances18Sized, …

Sized ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Sized QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
Sized RawTopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName
Sized TopLevelModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.TopLevelModuleName · orphan
Sized OccursWhereDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity.Occurrence
Sized PermutationDefined in Agda-2.7.0.1 · Agda.Utils.Permutation
Sized IntSetDefined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (Tele a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal
The size of a telescope is its length (as a list).
Sized (List1 a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (SizedThing a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Return the cached size.
Sized (IntMap a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (Seq a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (Set a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (HashSet a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized [a]Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized a => Sized (Abs a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal
Sized (Map k a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (HashMap k a)Defined in Agda-2.7.0.1 · Agda.Utils.Size

datadata SizedThing a

Thing decorated with its size. The thing should fit into main memory, thus, the size is an Int.

Instances2Null, Sized

Null a => Null (SizedThing a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Sized (SizedThing a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
Return the cached size.

valuesizeThing :: Sized a => a -> SizedThing a

Cache the size of an object.

datadata Peano

The natural numbers in (lazy) unary notation.

Instances11Bounded, Enum, Eq, Integral, Data, Num, …