| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 | Source

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

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 MutualId | Source

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