| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.MetaVars

Synopsis

getMetaStore :: MonadTCM tcm => tcm MetaStore
lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariable
updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm ()
getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPriority
isSortMeta :: MonadTCM tcm => MetaId -> tcm Bool
createMetaInfo :: MonadTCM tcm => tcm MetaInfo
updateMetaVarRange :: MonadTCM tcm => MetaId -> Range -> tcm ()
addInteractionPoint :: MonadTCM tcm => InteractionId -> MetaId -> tcm ()
removeInteractionPoint :: MonadTCM tcm => InteractionId -> tcm ()
getInteractionPoints :: MonadTCM tcm => tcm [InteractionId]
getInteractionMetas :: MonadTCM tcm => tcm [MetaId]
isInteractionMeta :: MonadTCM tcm => MetaId -> tcm Bool
lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId
judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId)
newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Judgement Type a -> tcm MetaId
newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Judgement Type a -> tcm MetaId
getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range
getMetaRange :: MonadTCM tcm => MetaId -> tcm Range
getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo
withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm a
getInstantiatedMetas :: MonadTCM tcm => tcm [MetaId]
getOpenMetas :: MonadTCM tcm => tcm [MetaId]
listenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
unlistenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId]
clearMetaListeners :: MonadTCM tcm => MetaId -> tcm ()

Documentation

getMetaStore :: MonadTCM tcm => tcm MetaStore | Source

Get the meta store.

lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariable | Source

Lookup a meta variable

updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm () | Source

getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPriority | Source

isSortMeta :: MonadTCM tcm => MetaId -> tcm Bool | Source

createMetaInfo :: MonadTCM tcm => tcm MetaInfo | Source

updateMetaVarRange :: MonadTCM tcm => MetaId -> Range -> tcm () | Source

addInteractionPoint :: MonadTCM tcm => InteractionId -> MetaId -> tcm () | Source

removeInteractionPoint :: MonadTCM tcm => InteractionId -> tcm () | Source

getInteractionPoints :: MonadTCM tcm => tcm [InteractionId] | Source

getInteractionMetas :: MonadTCM tcm => tcm [MetaId] | Source

isInteractionMeta :: MonadTCM tcm => MetaId -> tcm Bool | Source

Does the meta variable correspond to an interaction point?

lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId | Source

judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId) | Source

newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Judgement Type a -> tcm MetaId | Source

Generate new meta variable.

newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Judgement Type a -> tcm MetaId | Source

getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range | Source

getMetaRange :: MonadTCM tcm => MetaId -> tcm Range | Source

getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo | Source

withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm a | Source

getInstantiatedMetas :: MonadTCM tcm => tcm [MetaId] | Source

getOpenMetas :: MonadTCM tcm => tcm [MetaId] | Source

listenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm () | Source

`listenToMeta l m`: register `l` as a listener to `m`. This is done when the type of l is blocked by `m`.

unlistenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm () | Source

Unregister a listener.

getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId] | Source

Get the listeners to a meta.

clearMetaListeners :: MonadTCM tcm => MetaId -> tcm () | Source

Produced by Haddock version 2.4.2