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

Agda.TypeChecking.Monad.Mutual

Synopsis

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.