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

Agda.TypeChecking.Monad.Mutual

Synopsis

- noMutualBlock :: MonadTCM tcm => tcm a -> tcm a
- inMutualBlock :: MonadTCM tcm => tcm a -> tcm a
- setMutualBlock :: MonadTCM tcm => MutualId -> QName -> tcm ()
- getMutualBlocks :: MonadTCM tcm => tcm [Set QName]
- currentMutualBlock :: MonadTCM tcm => tcm MutualId
- lookupMutualBlock :: MonadTCM tcm => MutualId -> tcm (Set QName)
- findMutualBlock :: MonadTCM tcm => QName -> tcm (Set QName)

# Documentation

noMutualBlock :: MonadTCM tcm => tcm a -> tcm a

inMutualBlock :: MonadTCM tcm => tcm a -> tcm a

setMutualBlock :: MonadTCM tcm => MutualId -> QName -> tcm ()

Set the mutual block for a definition

getMutualBlocks :: MonadTCM tcm => tcm [Set QName]

Get all mutual blocks

currentMutualBlock :: MonadTCM tcm => tcm MutualId

Get the current mutual block.

lookupMutualBlock :: MonadTCM tcm => MutualId -> tcm (Set QName)

findMutualBlock :: MonadTCM tcm => QName -> tcm (Set QName)