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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Null

Contents

Description

Overloaded null and empty for collections and sequences.

Synopsis

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 () # 

Methods

empty :: () #

null :: () -> Bool #

Null ByteString # 
Null IntSet # 

Methods

empty :: IntSet #

null :: IntSet -> Bool #

Null Doc # 

Methods

empty :: Doc #

null :: Doc -> Bool #

Null Permutation # 
Null Occurrence # 
Null PatInfo # 

Methods

empty :: PatInfo #

null :: PatInfo -> Bool #

Null LHSInfo # 

Methods

empty :: LHSInfo #

null :: LHSInfo -> Bool #

Null MutualInfo #

Default value for MutualInfo.

Null LetInfo # 

Methods

empty :: LetInfo #

null :: LetInfo -> Bool #

Null ExprInfo # 

Methods

empty :: ExprInfo #

null :: ExprInfo -> Bool #

Null Clause #

A null clause is one with no patterns and no rhs. Should not exist in practice.

Methods

empty :: Clause #

null :: Clause -> Bool #

Null FreeVars # 

Methods

empty :: FreeVars #

null :: FreeVars -> Bool #

Null Simplification # 
Null Fields # 

Methods

empty :: Fields #

null :: Fields -> Bool #

Null ProjLams # 

Methods

empty :: ProjLams #

null :: ProjLams -> Bool #

Null MutualBlock # 
Null ProblemRest # 
Null Edge # 

Methods

empty :: Edge #

null :: Edge -> Bool #

Null NLMState # 

Methods

empty :: NLMState #

null :: NLMState -> Bool #

Null [a] # 

Methods

empty :: [a] #

null :: [a] -> Bool #

Null (Maybe a) #

A Maybe is null when it corresponds to the empty list.

Methods

empty :: Maybe a #

null :: Maybe a -> Bool #

Null (IntMap a) # 

Methods

empty :: IntMap a #

null :: IntMap a -> Bool #

Null (Seq a) # 

Methods

empty :: Seq a #

null :: Seq a -> Bool #

Null (Set a) # 

Methods

empty :: Set a #

null :: Set a -> Bool #

Null (HashSet a) # 

Methods

empty :: HashSet a #

null :: HashSet a -> Bool #

Null (Bag a) # 

Methods

empty :: Bag a #

null :: Bag a -> Bool #

Null (Favorites a) # 

Methods

empty :: Favorites a #

null :: Favorites a -> Bool #

Null a => Null (SizedThing a) # 

Methods

empty :: SizedThing a #

null :: SizedThing a -> Bool #

Null (Benchmark a) #

Initial benchmark structure (empty).

Methods

empty :: Benchmark a #

null :: Benchmark a -> Bool #

Null (CMSet cinfo) # 

Methods

empty :: CMSet cinfo #

null :: CMSet cinfo -> Bool #

Null (CallGraph cinfo) #

null checks whether the call graph is completely disconnected.

Methods

empty :: CallGraph cinfo #

null :: CallGraph cinfo -> Bool #

Null (Range' a) # 

Methods

empty :: Range' a #

null :: Range' a -> Bool #

Null (TCM Doc) # 

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.

Null (Substitution' a) # 
Null (Tele a) # 

Methods

empty :: Tele a #

null :: Tele a -> Bool #

Null (Case m) # 

Methods

empty :: Case m #

null :: Case m -> Bool #

Null (Match a) # 

Methods

empty :: Match a #

null :: Match a -> Bool #

Null a => Null (Problem' a) # 

Methods

empty :: Problem' a #

null :: Problem' a -> Bool #

Null a => Null (MaybeWarnings' a) # 
(Null a, Null b) => Null (a, b) # 

Methods

empty :: (a, b) #

null :: (a, b) -> Bool #

Null (Map k a) # 

Methods

empty :: Map k a #

null :: Map k a -> Bool #

Null (HashMap k a) # 

Methods

empty :: HashMap k a #

null :: HashMap k a -> Bool #

Null (Trie k v) #

Empty 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 () #