Agda.TypeChecking.Monad.MetaVars

dontAssignMetas

getMetaStore

modifyMetaStore

lookupMeta

updateMetaVar

getMetaPriority

isSortMeta

isSortMeta_

getMetaType

getMetaTypeInContext

class IsInstantiatedMeta a

isInstantiatedMeta'

createMetaInfo

createMetaInfo'

setValueMetaName

getMetaNameSuggestion

setMetaNameSuggestion

updateMetaVarRange

Query and manipulate interaction points.

modifyInteractionPoints

registerInteractionPoint

connectInteractionPoint

removeInteractionPoint

getInteractionPoints

getInteractionMetas

getInteractionIdsAndMetas

isInteractionMeta

lookupInteractionPoint

lookupInteractionId

newMeta

newMeta'

getInteractionRange

getMetaRange

getInteractionScope

withMetaInfo'

withMetaInfo

getInstantiatedMetas

getOpenMetas

listenToMeta

unlistenToMeta

getMetaListeners

clearMetaListeners

Freezing and unfreezing metas.

withFreezeMetas

freezeMetas

unfreezeMetas

unfreezeMetas'

isFrozen

class UnFreezeMeta a