unless package:Agda

The more general type Null m => [a] -> (List1 a -> m) -> m often causes type inference to fail, as we do not in general have instance Applicative m => Null (m ()).

A more general type would be Null m => Map k a -> (Map1 k a -> m) -> m but this type is problematic as we do not have a general instance Applicative m => Null (m ()).

A more general type would be Null m => Set a -> (Set1 a -> m) -> m but this type is problematic as we do not have a general instance Applicative m => Null (m ()).

Use hard compile-time mode in the continuation if the first argument is Erased something. Use run-time mode if the first argument is NotErased something and the current mode is not hard compile-time mode.

Use run-time mode in the continuation unless the current mode is the hard compile-time mode.

applyUnless b f a applies f to a unless b.

applyUnlessIts p f a applies f to a unless p a.

Monadic version of applyUnless