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

Safe HaskellNone
LanguageHaskell98

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 MutualId Source

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