Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

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 :: 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.

setMutualBlock :: MutualId -> QName -> TCM () Source #

Set the mutual block for a definition.

currentOrFreshMutualBlock :: TCM MutualId Source #

Get the current mutual block, if any, otherwise a fresh mutual block is returned.

lookupMutualBlock :: MutualId -> TCM MutualBlock Source #

mutualBlockOf :: QName -> TCM MutualId Source #

Reverse lookup of a mutual block id for a names.