Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.Null

Contents

- Testing for null.

Description

Overloaded `null` and `empty` for collections and sequences.

Synopsis

- class Null a where
  - empty :: a
  - null :: a -> Bool
- ifNull :: Null a => a -> b -> (a -> b) -> b
- ifNotNull :: Null a => a -> (a -> b) -> b -> b
- ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> m b) -> m b
- ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> m b -> m b
- whenNull :: (Monad m, Null a) => a -> m () -> m ()
- unlessNull :: (Monad m, Null a) => a -> (a -> m ()) -> m ()
- whenNullM :: (Monad m, Null a) => m a -> m () -> m ()
- unlessNullM :: (Monad m, Null a) => m a -> (a -> m ()) -> m ()

# Documentation

class Null a where Source #

Minimal complete definition

empty

Methods

empty :: a Source #

null :: a -> Bool Source #

Satisfying `null empty == True`.

null :: Eq a => a -> Bool Source #

Satisfying `null empty == True`.

Instances

Null () Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: () Source # null :: () -> Bool Source #
Null ByteString Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: ByteString Source # null :: ByteString -> Bool Source #
Null IntSet Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: IntSet Source # null :: IntSet -> Bool Source #
Null Doc Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Doc Source # null :: Doc -> Bool Source #
Null Permutation Source # |
Instance details Defined in Agda.Utils.Permutation Methods empty :: Permutation Source # null :: Permutation -> Bool Source #
Null Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence Source # null :: Occurrence -> Bool Source #
Null PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo Source # null :: PatInfo -> Bool Source #
Null LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo Source # null :: LHSInfo -> Bool Source #
Null MutualInfo Source # | Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo Source # null :: MutualInfo -> Bool Source #
Null LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo Source # null :: LetInfo -> Bool Source #
Null ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo Source # null :: ExprInfo -> Bool Source #
Null Clause Source # | A `null` clause is one with no patterns and no rhs. Should not exist in practice.
Instance details Defined in Agda.Syntax.Internal Methods empty :: Clause Source # null :: Clause -> Bool Source #
Null FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods empty :: FreeVars Source # null :: FreeVars -> Bool Source #
Null Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Simplification Source # null :: Simplification -> Bool Source #
Null Fields Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Fields Source # null :: Fields -> Bool Source #
Null ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: ProjLams Source # null :: ProjLams -> Bool Source #
Null MutualBlock Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: MutualBlock Source # null :: MutualBlock -> Bool Source #
Null NLMState Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods empty :: NLMState Source # null :: NLMState -> Bool Source #
Null [a] Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: [a] Source # null :: [a] -> Bool Source #
Null (Maybe a) Source # | A `Maybe` is `null` when it corresponds to the empty list.
Instance details Defined in Agda.Utils.Null Methods empty :: Maybe a Source # null :: Maybe a -> Bool Source #
Null (IntMap a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: IntMap a Source # null :: IntMap a -> Bool Source #
Null (Seq a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Seq a Source # null :: Seq a -> Bool Source #
Null (Set a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Set a Source # null :: Set a -> Bool Source #
Null (Maybe a) Source # |
Instance details Defined in Agda.Utils.Maybe.Strict Methods empty :: Maybe a Source # null :: Maybe a -> Bool Source #
Null (HashSet a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: HashSet a Source # null :: HashSet a -> Bool Source #
Null (Bag a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Bag a Source # null :: Bag a -> Bool Source #
Null a => Null (SizedThing a) Source # |
Instance details Defined in Agda.Utils.Size Methods empty :: SizedThing a Source # null :: SizedThing a -> Bool Source #
Null (Benchmark a) Source # | Initial benchmark structure (empty).
Instance details Defined in Agda.Utils.Benchmark Methods empty :: Benchmark a Source # null :: Benchmark a -> Bool Source #
Null (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a Source # null :: Range' a -> Bool Source #
Null (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
Null (WhereClause' a) Source # | A `WhereClause` is `null` when the `where` keyword is absent. An empty list of declarations does not count as `null` here.
Instance details Defined in Agda.Syntax.Concrete Methods empty :: WhereClause' a Source # null :: WhereClause' a -> Bool Source #
Null (Favorites a) Source # |
Instance details Defined in Agda.Utils.Favorites Methods empty :: Favorites a Source # null :: Favorites a -> Bool Source #
Null (CMSet cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods empty :: CMSet cinfo Source # null :: CMSet cinfo -> Bool Source #
Null (CallGraph cinfo) Source # | `null` checks whether the call graph is completely disconnected.
Instance details Defined in Agda.Termination.CallGraph Methods empty :: CallGraph cinfo Source # null :: CallGraph cinfo -> Bool Source #
Null (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
Null (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Tele a Source # null :: Tele a -> Bool Source #
Null (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods empty :: Case m Source # null :: Case m -> Bool Source #
Null (Match a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods empty :: Match a Source # null :: Match a -> Bool Source #
Null a => Null (MaybeWarnings' a) Source # |
Instance details Defined in Agda.Interaction.Imports Methods empty :: MaybeWarnings' a Source # null :: MaybeWarnings' a -> Bool Source #
(Null a, Null b) => Null (a, b) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: (a, b) Source # null :: (a, b) -> Bool Source #
Null (HashMap k a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: HashMap k a Source # null :: HashMap k a -> Bool Source #
Null (Map k a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Map k a Source # null :: Map k a -> Bool Source #
Null (Solution rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods empty :: Solution rigid flex Source # null :: Solution rigid flex -> Bool Source #
Null (Trie k v) Source # | Empty trie.
Instance details Defined in Agda.Utils.Trie Methods empty :: Trie k v Source # null :: Trie k v -> Bool Source #

# Testing for null.

ifNull :: Null a => a -> b -> (a -> b) -> b Source #

ifNotNull :: Null a => a -> (a -> b) -> b -> b Source #

ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> m b) -> m b Source #

ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> m b -> m b Source #

whenNull :: (Monad m, Null a) => a -> m () -> m () Source #

unlessNull :: (Monad m, Null a) => a -> (a -> m ()) -> m () Source #

whenNullM :: (Monad m, Null a) => m a -> m () -> m () Source #

unlessNullM :: (Monad m, Null a) => m a -> (a -> m ()) -> m () Source #