Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Size

Description

Collection size.

For TermSize see Agda.Syntax.Internal.

Synopsis

Documentation

class Sized a where Source #

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

Minimal complete definition

Nothing

Methods

size :: a -> Int Source #

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 :: forall (t :: Type -> Type) b. (Foldable t, t b ~ a) => a -> Int Source #

natSize :: a -> Peano Source #

Lazily compute a (possibly infinite) size.

Use when comparing a size against a fixed number.

default natSize :: forall (t :: Type -> Type) b. (Foldable t, t b ~ a) => a -> Peano Source #

Instances

Instances details
Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Sized TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Sized OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Sized Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Sized IntSet Source # 
Instance details

Defined in Agda.Utils.Size

Sized a => Sized (Abs a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

natSize :: Abs a -> Peano 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 #

natSize :: Tele a -> Peano Source #

Sized (List1 a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: List1 a -> Int Source #

natSize :: List1 a -> Peano Source #

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

Sized (IntMap a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: IntMap a -> Int Source #

natSize :: IntMap a -> Peano Source #

Sized (Seq a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Seq a -> Int Source #

natSize :: Seq a -> Peano Source #

Sized (Set a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Set a -> Int Source #

natSize :: Set a -> Peano Source #

Sized (HashSet a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashSet a -> Int Source #

natSize :: HashSet a -> Peano Source #

Sized [a] Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: [a] -> Int Source #

natSize :: [a] -> Peano Source #

Sized (Map k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: Map k a -> Int Source #

natSize :: Map k a -> Peano Source #

Sized (HashMap k a) Source # 
Instance details

Defined in Agda.Utils.Size

Methods

size :: HashMap k a -> Int Source #

natSize :: HashMap k a -> Peano 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

Instances

Instances details
Null a => Null (SizedThing a) Source # 
Instance details

Defined in Agda.Utils.Size

Sized (SizedThing a) Source #

Return the cached size.

Instance details

Defined in Agda.Utils.Size

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

Cache the size of an object.

data Peano #

Constructors

Zero 
Succ Peano 

Instances

Instances details
Data Peano 
Instance details

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 
Instance details

Defined in Data.Peano

Enum Peano 
Instance details

Defined in Data.Peano

Ix Peano 
Instance details

Defined in Data.Peano

Num Peano 
Instance details

Defined in Data.Peano

Read Peano 
Instance details

Defined in Data.Peano

Integral Peano 
Instance details

Defined in Data.Peano

Real Peano 
Instance details

Defined in Data.Peano

Methods

toRational :: Peano -> Rational #

Show Peano 
Instance details

Defined in Data.Peano

Methods

showsPrec :: Int -> Peano -> ShowS #

show :: Peano -> String #

showList :: [Peano] -> ShowS #

Eq Peano 
Instance details

Defined in Data.Peano

Methods

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

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

Ord Peano 
Instance details

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 #