unless package:Agda -is:exact

The reverse of when.
applyUnless b f a applies f to a unless b.
Monadic version of applyUnless