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

Safe HaskellSafe-Infered

Agda.TypeChecking.Monad.MetaVars

Synopsis

Documentation

getMetaStore :: TCM MetaStore

Get the meta store.

lookupMeta :: MetaId -> TCM MetaVariable

Lookup a meta variable

isInteractionMeta :: MetaId -> TCM Bool

Does the meta variable correspond to an interaction point?

newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId

Generate new meta variable.

newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

listenToMeta :: Listener -> 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 :: Listener -> MetaId -> TCM ()

Unregister a listener.

getMetaListeners :: MetaId -> TCM [Listener]

Get the listeners to a meta.

freezeMetas :: TCM ()

Freeze all meta variables.