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.6.0