Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred

Agda.Utils.Fresh

Description

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

# Documentation

class HasFresh i a where

Methods

nextFresh :: a -> (i, a)

Instances

HasFresh Int FreshThings |
HasFresh i FreshThings => HasFresh i TCState |
HasFresh NameId FreshThings |
HasFresh MetaId FreshThings |
HasFresh CtxId FreshThings |
HasFresh MutualId FreshThings |
HasFresh InteractionId FreshThings |
HasFresh ProblemId FreshThings |

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

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