unless package:Agda

The reverse of when.
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.
Monadic version of applyUnless