Agda-2.2.10: A dependently typed functional programming language and proof assistant
Agda.Utils.Fresh
Description
A common interface for monads which allow some kind of fresh name generation.
class HasFresh i a where
Methods
nextFresh :: a -> (i, a)
Instances
fresh :: (HasFresh i s, MonadState s m) => m i
withFresh :: (HasFresh i e, MonadReader e m) => (i -> m a) -> m a