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

Agda.TypeChecking.Monad.MetaVars

Synopsis

Documentation

getMetaStore :: MonadTCM tcm => tcm MetaStore

Get the meta store.

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

Lookup a meta variable

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

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

Does the meta variable correspond to an interaction point?

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

Generate new meta variable.

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

getOpenMetas :: MonadTCM tcm => tcm [MetaId]

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

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 ()

Unregister a listener.

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

Get the listeners to a meta.