Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 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
Produced by Haddock version 2.4.2