Agda-2.2.10: 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.6.1