when package:Agda

Conditional execution of Applicative expressions. For example,
when debug (putStrLn "Debugging")
will output the string Debugging if the Boolean value debug is True, and otherwise do nothing.
Run a computation if a certain verbosity level is activated (exact match).
Run some code when the given profiling option is active.
Freeze metas created by given computation if in abstract mode.
A more telling name for forM_ for the Maybe collection type. Or: caseMaybe without the Nothing case.
caseMaybeM without the Nothing case.
caseMaybe without the Just case.
caseMaybeM without the Just case.
A more telling name for forM for the Maybe collection type. Or: caseMaybe without the Nothing case.
Apply a function if a certain verbosity level is activated. Precondition: The level must be non-negative.
A variant of instantiateFull that only instantiates those meta-variables that satisfy the predicate.
applyWhen b f a applies f to a when b.
Maybe version of applyWhen.
Monadic version of applyWhen
Maybe version of applyUnless.
Chop a list at the positions when the predicate holds. Contrary to wordsBy, consecutive separator elements will result in an empty segment in the result. O(n).
intercalate [x] (chopWhen (== x) xs) == xs