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

Agda.TypeChecking.Monad.Mutual

Synopsis

Documentation

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

Set the mutual block for a definition

getMutualBlocks :: TCM [Set QName]Source

Get all mutual blocks

currentMutualBlock :: TCM MutualIdSource

Get the current mutual block.