ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Mutual
Synopsis
- value noMutualBlock
- value inMutualBlock
- value insertMutualBlockInfo
- value setMutualBlock
- value currentOrFreshMutualBlock
- value lookupMutualBlock
- PackageAgda-2.8.0.2
- Exports6
- LanguageHaskell2010
- LicenceMIT
- SourceMutual.hs
Pass the current mutual block id or create a new mutual block if we are not already inside on.
Set the mutual block info for a block if non-existing.
Set the mutual block for a definition.
Get the current mutual block, if any, otherwise a fresh mutual block is returned.