Agda-2.3.2: 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 whereSource
Methods
nextFresh :: a -> (i, a)Source
Instances
fresh :: (HasFresh i s, MonadState s m) => m iSource
withFresh :: (HasFresh i e, MonadReader e m) => (i -> m a) -> m aSource