| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Mutual
Synopsis
- noMutualBlock :: TCM a -> TCM a
- inMutualBlock :: (MutualId -> TCM a) -> TCM a
- setMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
- insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
- setMutualBlock :: MutualId -> QName -> TCM ()
- currentOrFreshMutualBlock :: TCM MutualId
- lookupMutualBlock :: ReadTCState tcm => MutualId -> tcm MutualBlock
- mutualBlockOf :: QName -> TCM MutualId
Documentation
noMutualBlock :: TCM a -> TCM a Source #
inMutualBlock :: (MutualId -> TCM a) -> TCM a Source #
Pass the current mutual block id or create a new mutual block if we are not already inside on.
setMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #
Set the mutual block info for a block, possibly overwriting the existing one.
insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #
Set the mutual block info for a block if non-existing.
currentOrFreshMutualBlock :: TCM MutualId Source #
Get the current mutual block, if any, otherwise a fresh mutual block is returned.
lookupMutualBlock :: ReadTCState tcm => MutualId -> tcm MutualBlock Source #