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

Safe HaskellNone

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

currentOrFreshMutualBlock :: TCM MutualIdSource

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