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.

Documentation

class HasFresh i a whereSource

Methods

nextFresh :: a -> (i, a)Source

fresh :: (HasFresh i s, MonadState s m) => m iSource

withFresh :: (HasFresh i e, MonadReader e m) => (i -> m a) -> m aSource