ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Size

Collection size.

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

Instances13Bounded, Enum, Eq, Integral, Data, Num, …

Bounded PeanoDefined in peano-0.1.1.0 · Data.Peano
Enum PeanoDefined in peano-0.1.1.0 · Data.Peano
Eq PeanoDefined in peano-0.1.1.0 · Data.Peano
Integral PeanoDefined in peano-0.1.1.0 · Data.Peano
Data PeanoDefined in peano-0.1.1.0 · Data.Peano
Num PeanoDefined in peano-0.1.1.0 · Data.Peano
Ord PeanoDefined in peano-0.1.1.0 · Data.Peano
Read PeanoDefined in peano-0.1.1.0 · Data.Peano
Real PeanoDefined in peano-0.1.1.0 · Data.Peano
Show PeanoDefined in peano-0.1.1.0 · Data.Peano
Ix PeanoDefined in peano-0.1.1.0 · Data.Peano
Generic PeanoDefined in peano-0.1.1.0 · Data.Peano
type Rep Peano = D1 ('MetaData "Peano" "Data.Peano" "peano-0.1.1.0-JzRPaouGkcPHGxkINor7Cl" 'False) (C1 ('MetaCons "Zero" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Succ" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Peano)))Defined in peano-0.1.1.0 · Data.Peano