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

Synopsis

# Documentation

dontAssignMetas :: TCM a -> TCM a Source #

Switch off assignment of metas.

Get the meta store.

Lookup a meta variable

Given a meta, return the type applied to the current context.

class IsInstantiatedMeta a where Source #

Check whether all metas are instantiated. Precondition: argument is a meta (in some form) or a list of metas.

Minimal complete definition

isInstantiatedMeta

Methods

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsisInstantiatedMeta :: [a] -> TCM Bool Source # Source # Methods Source # Methods Source # Does not worry about raising. Methods

Create MetaInfo in the current environment.

# Query and manipulate interaction points.

Register an interaction point during scope checking. If there is no interaction id yet, create one.

Hook up meta variable to interaction point.

Move an interaction point from the current ones to the old ones.

Get a list of interaction ids.

Get all metas that correspond to interaction ids.

Get all metas that correspond to interaction ids.

Does the meta variable correspond to an interaction point?

Time: O(n) where n is the number of interaction metas.

Get the information associated to an interaction point.

Get MetaId for an interaction point. Precondition: interaction point is connected.

Generate new meta variable.

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

Get the Range for an interaction point.

Get the Range for a meta variable.

listenToMeta l m: register l as a listener to m. This is done when the type of l is blocked by m.

Unregister a listener.

Get the listeners to a meta.

# Freezing and unfreezing metas.

withFreezeMetas :: TCM a -> TCM a Source #

Freeze all so far unfrozen metas for the duration of the given computation.

Freeze all meta variables and return the list of metas that got frozen.

Thaw all meta variables.

unfreezeMetas' :: (MetaId -> Bool) -> TCM () Source #

Thaw some metas, as indicated by the passed condition.

class UnFreezeMeta a where Source #

Unfreeze meta and its type if this is a meta again. Does not unfreeze deep occurrences of metas.

Minimal complete definition

unfreezeMeta

Methods

unfreezeMeta :: a -> TCM () Source #

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods UnFreezeMeta a => UnFreezeMeta [a] Source # MethodsunfreezeMeta :: [a] -> TCM () Source # UnFreezeMeta a => UnFreezeMeta (Abs a) Source # MethodsunfreezeMeta :: Abs a -> TCM () Source #