Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
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
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 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.
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.6.1