Agda-2.2.8: A dependently typed functional programming language and proof assistant




getMetaStore :: MonadTCM tcm => tcm MetaStoreSource

Get the meta store.

lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariableSource

Lookup a meta variable

isInteractionMeta :: MonadTCM tcm => MetaId -> tcm BoolSource

Does the meta variable correspond to an interaction point?

newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaIdSource

Generate new meta variable.

withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm aSource

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.