| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Size
Description
Collection size.
For TermSize see Agda.Syntax.Internal.
Synopsis
- class Sized a where
- data SizedThing a = SizedThing {
- theSize :: !Int
- sizedThing :: a
- sizeThing :: Sized a => a -> SizedThing a
- data Peano
Documentation
The size of a collection (i.e., its length).
Minimal complete definition
Nothing
Methods
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.
natSize :: a -> Peano Source #
Lazily compute a (possibly infinite) size.
Use when comparing a size against a fixed number.
Instances
| Sized ModuleName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
| Sized QName Source # | |
| Sized RawTopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName Methods size :: RawTopLevelModuleName -> Int Source # natSize :: RawTopLevelModuleName -> Peano Source # | |
| Sized TopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName | |
| Sized OccursWhere Source # | |
Defined in Agda.TypeChecking.Positivity.Occurrence | |
| Sized Permutation Source # | |
Defined in Agda.Utils.Permutation | |
| Sized IntSet Source # | |
| Sized a => Sized (Abs a) Source # | |
| Sized (Tele a) Source # | The size of a telescope is its length (as a list). |
| Sized (List1 a) Source # | |
| Sized (SizedThing a) Source # | Return the cached size. |
Defined in Agda.Utils.Size | |
| Sized (IntMap a) Source # | |
| Sized (Seq a) Source # | |
| Sized (Set a) Source # | |
| Sized (HashSet a) Source # | |
| Sized [a] Source # | |
| Sized (Map k a) Source # | |
| Sized (HashMap k a) 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
| Null a => Null (SizedThing a) Source # | |
Defined in Agda.Utils.Size | |
| Sized (SizedThing a) Source # | Return the cached size. |
Defined in Agda.Utils.Size | |
sizeThing :: Sized a => a -> SizedThing a Source #
Cache the size of an object.
The natural numbers in (lazy) unary notation.
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 # 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 # | |
| Enum Peano # | |
| Ix Peano # | |
| Num Peano # | |
| Read Peano # | |
| Integral Peano # | |
| Real Peano # | |
Defined in Data.Peano Methods toRational :: Peano -> Rational # | |
| Show Peano # | |
| Eq Peano # | |
| Ord Peano # | |