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