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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Monad.Mutual

Synopsis

- noMutualBlock :: TCM a -> TCM a
- inMutualBlock :: TCM a -> TCM a
- setMutualBlock :: MutualId -> QName -> TCM ()
- getMutualBlocks :: TCM [Set QName]
- currentMutualBlock :: 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

currentMutualBlock :: TCM MutualId

Get the current mutual block.

lookupMutualBlock :: MutualId -> TCM (Set QName)

findMutualBlock :: QName -> TCM (Set QName)