Agda.TypeChecking.Monad.MetaVars
- 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
- isInstantiatedMeta :: 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 -> Permutation -> Judgement Type a -> tcm MetaId
- newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> 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 MetaStoreSource
Get the meta store.
lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariableSource
Lookup a meta variable
updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm ()Source
getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPrioritySource
isSortMeta :: MonadTCM tcm => MetaId -> tcm BoolSource
isInstantiatedMeta :: MonadTCM tcm => MetaId -> tcm BoolSource
createMetaInfo :: MonadTCM tcm => tcm MetaInfoSource
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 BoolSource
Does the meta variable correspond to an interaction point?
lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaIdSource
judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId)Source
newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaIdSource
Generate new meta variable.
newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaIdSource
getInteractionRange :: MonadTCM tcm => InteractionId -> tcm RangeSource
getMetaRange :: MonadTCM tcm => MetaId -> tcm RangeSource
getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfoSource
withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm aSource
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.
getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId]Source
Get the listeners to a meta.
clearMetaListeners :: MonadTCM tcm => MetaId -> tcm ()Source