| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.Fresh

Description
A common interface for monads which allow some kind of fresh name generation.
Documentation

class HasFresh i a where | Source

Methods

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

Instances

HasFresh Integer FreshThings
HasFresh Integer FreshThings
HasFresh i FreshThings => HasFresh i TCState
HasFresh NameId FreshThings
HasFresh NameId FreshThings
HasFresh MetaId FreshThings
HasFresh MetaId FreshThings
HasFresh CtxId FreshThings
HasFresh CtxId FreshThings
HasFresh MutualId FreshThings
HasFresh MutualId FreshThings
HasFresh InteractionId FreshThings
HasFresh InteractionId FreshThings

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

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

Produced by Haddock version 2.4.2