Agda.Utils.Size

Collection size.

For TermSize see Agda.Syntax.Internal.

Documentation

class Sized a where

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

Minimal complete definition

Nothing

Methods

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 .

default size :: (Foldable t, t b ~ a) => a -> Int

natSize :: a -> Peano

Lazily compute a (possibly infinite) size.

Use when comparing a size against a fixed number.

default natSize :: (Foldable t, t b ~ a) => a -> Peano

Instances

Sized ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int

natSize :: ModuleName -> Peano

Sized QName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int

natSize :: QName -> Peano

Sized RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: RawTopLevelModuleName -> Int

natSize :: RawTopLevelModuleName -> Peano

Sized TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

size :: TopLevelModuleName -> Int

natSize :: TopLevelModuleName -> Peano

Sized OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

size :: OccursWhere -> Int

natSize :: OccursWhere -> Peano

Sized Permutation

Defined in Agda.Utils.Permutation

Methods

size :: Permutation -> Int

natSize :: Permutation -> Peano

Sized IntSet

Defined in Agda.Utils.Size

Methods

size :: IntSet -> Int

natSize :: IntSet -> Peano

Sized a => Sized (Abs a)

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int

natSize :: Abs a -> Peano

Sized (Tele a)

The size of a telescope is its length (as a list).

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int

natSize :: Tele a -> Peano

Sized (List1 a)

Defined in Agda.Utils.Size

Methods

size :: List1 a -> Int

natSize :: List1 a -> Peano

Sized (SizedThing a)

Return the cached size.

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int

natSize :: SizedThing a -> Peano

Sized (IntMap a)

Defined in Agda.Utils.Size

Methods

size :: IntMap a -> Int

natSize :: IntMap a -> Peano

Sized (Seq a)

Defined in Agda.Utils.Size

Methods

size :: Seq a -> Int

natSize :: Seq a -> Peano

Sized (Set a)

Defined in Agda.Utils.Size

Methods

size :: Set a -> Int

natSize :: Set a -> Peano

Sized (HashSet a)

Defined in Agda.Utils.Size

Methods

size :: HashSet a -> Int

natSize :: HashSet a -> Peano

Sized [a]

Defined in Agda.Utils.Size

Methods

size :: [a] -> Int

natSize :: [a] -> Peano

Sized (Map k a)

Defined in Agda.Utils.Size

Methods

size :: Map k a -> Int

natSize :: Map k a -> Peano

Sized (HashMap k a)

Defined in Agda.Utils.Size

Methods

size :: HashMap k a -> Int

natSize :: HashMap k a -> Peano

data SizedThing a

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

Null a => Null (SizedThing a)

Defined in Agda.Utils.Size

Methods

empty :: SizedThing a

null :: SizedThing a -> Bool

Sized (SizedThing a)

Return the cached size.

Defined in Agda.Utils.Size

Methods

size :: SizedThing a -> Int

natSize :: SizedThing a -> Peano

sizeThing :: Sized a => a -> SizedThing a

Cache the size of an object.

data Peano

Constructors

Zero

Succ Peano

Instances

Data Peano

Defined in Data.Peano

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Peano -> c Peano

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Peano

toConstr :: Peano -> Constr

dataTypeOf :: Peano -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Peano)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)

gmapT :: (forall b. Data b => b -> b) -> Peano -> Peano

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r

gmapQ :: (forall d. Data d => d -> u) -> Peano -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Peano -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Peano -> m Peano

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano

Bounded Peano

Defined in Data.Peano

Methods

minBound :: Peano

maxBound :: Peano

Enum Peano

Defined in Data.Peano

Methods

succ :: Peano -> Peano

pred :: Peano -> Peano

toEnum :: Int -> Peano

fromEnum :: Peano -> Int

enumFrom :: Peano -> [Peano]

enumFromThen :: Peano -> Peano -> [Peano]

enumFromTo :: Peano -> Peano -> [Peano]

enumFromThenTo :: Peano -> Peano -> Peano -> [Peano]

Ix Peano

Defined in Data.Peano

Methods

range :: (Peano, Peano) -> [Peano]

index :: (Peano, Peano) -> Peano -> Int

unsafeIndex :: (Peano, Peano) -> Peano -> Int

inRange :: (Peano, Peano) -> Peano -> Bool

rangeSize :: (Peano, Peano) -> Int

unsafeRangeSize :: (Peano, Peano) -> Int

Num Peano

Defined in Data.Peano

Methods

(+) :: Peano -> Peano -> Peano

(-) :: Peano -> Peano -> Peano

(*) :: Peano -> Peano -> Peano

negate :: Peano -> Peano

abs :: Peano -> Peano

signum :: Peano -> Peano

fromInteger :: Integer -> Peano

Read Peano

Defined in Data.Peano

Methods

readsPrec :: Int -> ReadS Peano

readList :: ReadS [Peano]

readPrec :: ReadPrec Peano

readListPrec :: ReadPrec [Peano]

Integral Peano

Defined in Data.Peano

Methods

quot :: Peano -> Peano -> Peano

rem :: Peano -> Peano -> Peano

div :: Peano -> Peano -> Peano

mod :: Peano -> Peano -> Peano

quotRem :: Peano -> Peano -> (Peano, Peano)

divMod :: Peano -> Peano -> (Peano, Peano)

toInteger :: Peano -> Integer

Real Peano

Defined in Data.Peano

Methods

toRational :: Peano -> Rational

Show Peano

Defined in Data.Peano

Methods

showsPrec :: Int -> Peano -> ShowS

show :: Peano -> String

showList :: [Peano] -> ShowS

Eq Peano

Defined in Data.Peano

Methods

(==) :: Peano -> Peano -> Bool

(/=) :: Peano -> Peano -> Bool

Ord Peano

Defined in Data.Peano

Methods

compare :: Peano -> Peano -> Ordering

(<) :: Peano -> Peano -> Bool

(<=) :: Peano -> Peano -> Bool

(>) :: Peano -> Peano -> Bool

(>=) :: Peano -> Peano -> Bool

max :: Peano -> Peano -> Peano

min :: Peano -> Peano -> Peano