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
ifNull :: Null a => a -> b -> (a -> b) -> b
ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> 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 #

Minimal complete definition

empty

Methods

empty :: a #

null :: a -> Bool #

Satisfying null empty == True.

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

Satisfying null empty == True.

Instances

Null () #
Instance details Defined in Agda.Utils.Null Methods empty :: () # null :: () -> Bool #
Null ByteString #
Instance details Defined in Agda.Utils.Null Methods empty :: ByteString # null :: ByteString -> Bool #
Null IntSet #
Instance details Defined in Agda.Utils.Null Methods empty :: IntSet # null :: IntSet -> Bool #
Null Doc #
Instance details Defined in Agda.Utils.Null Methods empty :: Doc # null :: Doc -> Bool #
Null Permutation #
Instance details Defined in Agda.Utils.Permutation Methods empty :: Permutation # null :: Permutation -> Bool #
Null Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence # null :: Occurrence -> Bool #
Null PatInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo # null :: PatInfo -> Bool #
Null LHSInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo # null :: LHSInfo -> Bool #
Null MutualInfo #	Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo # null :: MutualInfo -> Bool #
Null LetInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo # null :: LetInfo -> Bool #
Null ExprInfo #
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo # null :: ExprInfo -> Bool #
Null Clause #	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 # null :: Clause -> Bool #
Null FreeVars #
Instance details Defined in Agda.TypeChecking.Free Methods empty :: FreeVars # null :: FreeVars -> Bool #
Null Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Simplification # null :: Simplification -> Bool #
Null Fields #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Fields # null :: Fields -> Bool #
Null ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: ProjLams # null :: ProjLams -> Bool #
Null MutualBlock #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: MutualBlock # null :: MutualBlock -> Bool #
Null NLMState #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods empty :: NLMState # null :: NLMState -> Bool #
Null Edge #
Instance details Defined in Agda.TypeChecking.Positivity Methods empty :: Edge # null :: Edge -> Bool #
Null [a] #
Instance details Defined in Agda.Utils.Null Methods empty :: [a] # null :: [a] -> Bool #
Null (Maybe a) #	A `Maybe` is `null` when it corresponds to the empty list.
Instance details Defined in Agda.Utils.Null Methods empty :: Maybe a # null :: Maybe a -> Bool #
Null (IntMap a) #
Instance details Defined in Agda.Utils.Null Methods empty :: IntMap a # null :: IntMap a -> Bool #
Null (Seq a) #
Instance details Defined in Agda.Utils.Null Methods empty :: Seq a # null :: Seq a -> Bool #
Null (Set a) #
Instance details Defined in Agda.Utils.Null Methods empty :: Set a # null :: Set a -> Bool #
Null (Maybe a) #
Instance details Defined in Agda.Utils.Maybe.Strict Methods empty :: Maybe a # null :: Maybe a -> Bool #
Null (HashSet a) #
Instance details Defined in Agda.Utils.Null Methods empty :: HashSet a # null :: HashSet a -> Bool #
Null (Bag a) #
Instance details Defined in Agda.Utils.Null Methods empty :: Bag a # null :: Bag a -> Bool #
Null a => Null (SizedThing a) #
Instance details Defined in Agda.Utils.Size Methods empty :: SizedThing a # null :: SizedThing a -> Bool #
Null (Benchmark a) #	Initial benchmark structure (empty).
Instance details Defined in Agda.Utils.Benchmark Methods empty :: Benchmark a # null :: Benchmark a -> Bool #
Null (Range' a) #
Instance details Defined in Agda.Syntax.Position Methods empty :: Range' a # null :: Range' a -> Bool #
Null (TCM Doc) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc # null :: TCM Doc -> Bool #
Null (WhereClause' a) #	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 # null :: WhereClause' a -> Bool #
Null (Favorites a) #
Instance details Defined in Agda.Utils.Favorites Methods empty :: Favorites a # null :: Favorites a -> Bool #
Null (CMSet cinfo) #
Instance details Defined in Agda.Termination.CallMatrix Methods empty :: CMSet cinfo # null :: CMSet cinfo -> Bool #
Null (CallGraph cinfo) #	`null` checks whether the call graph is completely disconnected.
Instance details Defined in Agda.Termination.CallGraph Methods empty :: CallGraph cinfo # null :: CallGraph cinfo -> Bool #
Null (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a # null :: Substitution' a -> Bool #
Null (Tele a) #
Instance details Defined in Agda.Syntax.Internal Methods empty :: Tele a # null :: Tele a -> Bool #
Null (Case m) #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods empty :: Case m # null :: Case m -> Bool #
Null (Match a) #
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods empty :: Match a # null :: Match a -> Bool #
Null a => Null (MaybeWarnings' a) #
Instance details Defined in Agda.Interaction.Imports Methods empty :: MaybeWarnings' a # null :: MaybeWarnings' a -> Bool #
(Null a, Null b) => Null (a, b) #
Instance details Defined in Agda.Utils.Null Methods empty :: (a, b) # null :: (a, b) -> Bool #
Null (Map k a) #
Instance details Defined in Agda.Utils.Null Methods empty :: Map k a # null :: Map k a -> Bool #
Null (HashMap k a) #
Instance details Defined in Agda.Utils.Null Methods empty :: HashMap k a # null :: HashMap k a -> Bool #
Null (Solution rigid flex) #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods empty :: Solution rigid flex # null :: Solution rigid flex -> Bool #
Null (Trie k v) #	Empty trie.
Instance details Defined in Agda.Utils.Trie Methods empty :: Trie k v # null :: Trie k v -> Bool #

Testing for null.

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

ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> 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 () #