Agda.TypeChecking.Monad.MetaVars

dontAssignMetas

getMetaStore

modifyMetaStore

metasCreatedBy

lookupMeta

updateMetaVar

getMetaPriority

isSortMeta

isSortMeta_

getMetaType

getMetaTypeInContext

class IsInstantiatedMeta a

isInstantiatedMeta'

allMetas

createMetaInfo

createMetaInfo'

setValueMetaName

getMetaNameSuggestion

setMetaNameSuggestion

updateMetaVarRange

setMetaOccursCheck

Query and manipulate interaction points.

modifyInteractionPoints

registerInteractionPoint

findInteractionPoint_

connectInteractionPoint

removeInteractionPoint

getInteractionPoints

getInteractionMetas

getInteractionIdsAndMetas

isInteractionMeta

lookupInteractionPoint

lookupInteractionId

lookupInteractionMeta

lookupInteractionMeta_

newMeta

newMeta'

getInteractionRange

getMetaRange

getInteractionScope

withMetaInfo'

withMetaInfo

getInstantiatedMetas

getOpenMetas

isOpenMeta

listenToMeta

unlistenToMeta

getMetaListeners

clearMetaListeners

Freezing and unfreezing metas.

withFreezeMetas

freezeMetas

freezeMetas'

unfreezeMetas

unfreezeMetas'

isFrozen

class UnFreezeMeta a