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

Agda.TypeChecking.Monad.Mutual

Synopsis

Documentation

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

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

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

Set the mutual block for a definition

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

Get all mutual blocks

currentMutualBlock :: MonadTCM tcm => tcm MutualIdSource

Get the current mutual block.

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

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