| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Monad.Mutual
- noMutualBlock :: TCM a -> TCM a
- inMutualBlock :: TCM a -> TCM a
- setMutualBlock :: MutualId -> QName -> TCM ()
- getMutualBlocks :: TCM [Set QName]
- currentOrFreshMutualBlock :: TCM MutualId
- lookupMutualBlock :: MutualId -> TCM (Set QName)
- mutualBlockOf :: QName -> TCM MutualId
- findMutualBlock :: QName -> TCM (Set QName)
Documentation
noMutualBlock :: TCM a -> TCM a Source
inMutualBlock :: TCM a -> TCM a Source
setMutualBlock :: MutualId -> QName -> TCM () Source
Set the mutual block for a definition
getMutualBlocks :: TCM [Set QName] Source
Get all mutual blocks
currentOrFreshMutualBlock :: TCM MutualId Source
Get the current mutual block, if any, otherwise a fresh mutual block is returned.
mutualBlockOf :: QName -> TCM MutualId Source