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

Safe Haskell | None

Agda.TypeChecking.Monad.Mutual

Synopsis

- 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)
- findMutualBlock :: QName -> TCM (Set QName)

# Documentation

noMutualBlock :: TCM a -> TCM a

inMutualBlock :: TCM a -> TCM a

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

Set the mutual block for a definition

getMutualBlocks :: TCM [Set QName]

Get all mutual blocks

currentOrFreshMutualBlock :: TCM MutualId

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

lookupMutualBlock :: MutualId -> TCM (Set QName)

findMutualBlock :: QName -> TCM (Set QName)