Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Mutual
- 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 :: MutualId -> TCM MutualBlock
- mutualBlockOf :: QName -> TCM MutualId
Documentation
noMutualBlock :: TCM a -> TCM a #
inMutualBlock :: (MutualId -> TCM a) -> TCM a #
Pass the current mutual block id or create a new mutual block if we are not already inside on.
setMutualBlockInfo :: MutualId -> MutualInfo -> TCM () #
Set the mutual block info for a block, possibly overwriting the existing one.
insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM () #
Set the mutual block info for a block if non-existing.
setMutualBlock :: MutualId -> QName -> TCM () #
Set the mutual block for a definition.
currentOrFreshMutualBlock :: TCM MutualId #
Get the current mutual block, if any, otherwise a fresh mutual block is returned.
lookupMutualBlock :: MutualId -> TCM MutualBlock #
mutualBlockOf :: QName -> TCM MutualId #
Reverse lookup of a mutual block id for a names.