Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Monad.MetaVars

Contents

Query and manipulate interaction points.
Freezing and unfreezing metas.

Synopsis

data MetaKind
- = Records
- | SingletonRecords
- | Levels
allMetaKinds :: [MetaKind]
data KeepMetas
- = KeepMetas
- | RollBackMetas
class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver m where
- newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
- assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
- assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
- etaExpandMeta :: [MetaKind] -> MetaId -> m ()
- updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
- speculateMetas :: m () -> m KeepMetas -> m ()
dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
getMetaStore :: ReadTCState m => m MetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta_ :: MetaVariable -> Bool
getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m, HasBuiltins m) => MetaId -> m Type
isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
class IsInstantiatedMeta a where
- isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool
isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
constraintMetas :: Constraint -> TCM (Set MetaId)
createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo' :: (MonadTCEnv m, ReadTCState m) => RunMetaOccursCheck -> m MetaInfo
setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
- freshInteractionId :: m InteractionId
- modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
registerInteractionPoint :: forall m. MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m ()
removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionMetas :: ReadTCState m => m [MetaId]
getUniqueMetasRanges :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range]
getUnsolvedMetas :: (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: (MonadFail m, ReadTCState m) => m [Range]
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)]
isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint
lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
getInteractionRange :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) => InteractionId -> m Range
getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range
getInteractionScope :: InteractionId -> TCM ScopeInfo
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo :: Closure Range -> TCM a -> TCM a
getMetaVariableSet :: ReadTCState m => m IntSet
getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getInstantiatedMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: ReadTCState m => m [MetaId]
isOpenMeta :: MetaInstantiation -> Bool
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
withFreezeMetas :: TCM a -> TCM a
freezeMetas :: TCM [MetaId]
freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]
unfreezeMetas :: TCM ()
unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
class UnFreezeMeta a where
- unfreezeMeta :: MonadMetaSolver m => a -> m ()

Documentation

data MetaKind Source #

Various kinds of metavariables.

Constructors

Records	Meta variables of record type.
SingletonRecords	Meta variables of "hereditarily singleton" record type.
Levels	Meta variables of level type, if type-in-type is activated.

Instances

Instances details

Bounded MetaKind Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods minBound :: MetaKind # maxBound :: MetaKind #
Enum MetaKind Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods succ :: MetaKind -> MetaKind # pred :: MetaKind -> MetaKind # toEnum :: Int -> MetaKind # fromEnum :: MetaKind -> Int # enumFrom :: MetaKind -> [MetaKind] # enumFromThen :: MetaKind -> MetaKind -> [MetaKind] # enumFromTo :: MetaKind -> MetaKind -> [MetaKind] # enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind] #
Show MetaKind Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods showsPrec :: Int -> MetaKind -> ShowS # show :: MetaKind -> String # showList :: [MetaKind] -> ShowS #
Eq MetaKind Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods (==) :: MetaKind -> MetaKind -> Bool # (/=) :: MetaKind -> MetaKind -> Bool #

allMetaKinds :: [MetaKind] Source #

All possible metavariable kinds.

data KeepMetas Source #

Constructors

KeepMetas
RollBackMetas

class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver m where Source #

Monad service class for creating, solving and eta-expanding of metavariables.

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

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

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m () Source #

Assign to an open metavar which may not be frozen. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

Assignment is aborted by throwing a PatternErr via a call to patternViolation. This error is caught by catchConstraint during equality checking (compareAtom) and leads to restoration of the original constraints.

assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () Source #

Directly instantiate the metavariable. Skip pattern check, occurs check and frozen check. Used for eta expanding frozen metas.

etaExpandMeta :: [MetaKind] -> MetaId -> m () Source #

Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m () Source #

Update the status of the metavariable

speculateMetas :: m () -> m KeepMetas -> m () Source #

'speculateMetas fallback m' speculatively runs m, but if the result is RollBackMetas any changes to metavariables are rolled back and fallback is run instead.

Instances

Instances details

MonadMetaSolver TCM Source #
Instance details Defined in Agda.TypeChecking.MetaVars Methods newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source # assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM () Source # assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source # etaExpandMeta :: [MetaKind] -> MetaId -> TCM () Source # updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source # speculateMetas :: TCM () -> TCM KeepMetas -> TCM () Source #
(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> PureConversionT m MetaId Source # assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> PureConversionT m () Source # assignTerm' :: MetaId -> [Arg ArgName] -> Term -> PureConversionT m () Source # etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m () Source # updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m () Source # speculateMetas :: PureConversionT m () -> PureConversionT m KeepMetas -> PureConversionT m () Source #

dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a Source #

Switch off assignment of metas.

getMetaStore :: ReadTCState m => m MetaStore Source #

Get the meta store.

modifyMetaStore :: (MetaStore -> MetaStore) -> TCM () Source #

metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet) Source #

Run a computation and record which new metas it created.

lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable) Source #

Lookup a meta variable.

lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable Source #

metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type Source #

Type of a term or sort meta.

updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #

Update the information associated with a meta variable.

insertMetaVar :: MetaId -> MetaVariable -> TCM () Source #

Insert a new meta variable with associated information into the meta store.

getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority Source #

isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

isSortMeta_ :: MetaVariable -> Bool Source #

getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type Source #

getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args Source #

Compute the context variables that a meta should be applied to, accounting for pruning.

getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m, HasBuiltins m) => MetaId -> m Type Source #

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

isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize Source #

Is it a meta that might be generalized?

class IsInstantiatedMeta a where Source #

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

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool Source #

Instances

Instances details

IsInstantiatedMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #
IsInstantiatedMeta Level Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source #
IsInstantiatedMeta PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source #
IsInstantiatedMeta Term Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #	Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Maybe a -> m Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta [a] Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => [a] -> m Bool Source #

isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term) Source #

constraintMetas :: Constraint -> TCM (Set MetaId) Source #

Returns all metavariables in a constraint. Slightly complicated by the fact that blocked terms are represented by two meta variables. To find the second one we need to look up the meta listeners for the one in the UnBlock constraint. This is used for the purpose of deciding if a metavariable is constrained or if it can be generalized over (see Agda.TypeChecking.Generalize).

createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo Source #

Create MetaInfo in the current environment.

createMetaInfo' :: (MonadTCEnv m, ReadTCState m) => RunMetaOccursCheck -> m MetaInfo Source #

setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m () Source #

getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion Source #

setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m () Source #

setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m () Source #

Change the ArgInfo that will be used when generalizing over this meta.

updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m () Source #

setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m () Source #

Query and manipulate interaction points.

class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where Source #

Minimal complete definition

Nothing

Methods

freshInteractionId :: m InteractionId Source #

default freshInteractionId :: (MonadTrans t, MonadInteractionPoints n, t n ~ m) => m InteractionId Source #

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m () Source #

default modifyInteractionPoints :: (MonadTrans t, MonadInteractionPoints n, t n ~ m) => (InteractionPoints -> InteractionPoints) -> m () Source #

Instances

Instances details

MonadInteractionPoints TCM Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: TCM InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM () Source #
(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods freshInteractionId :: PureConversionT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m () Source #
MonadInteractionPoints m => MonadInteractionPoints (IdentityT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: IdentityT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> IdentityT m () Source #
MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: ReaderT r m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> ReaderT r m () Source #
MonadInteractionPoints m => MonadInteractionPoints (StateT s m) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: StateT s m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> StateT s m () Source #

registerInteractionPoint :: forall m. MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId Source #

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

findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId Source #

Find an interaction point by Range' by searching the whole map. Issue 3000: Don't consider solved interaction points.

O(n): linear in the number of registered interaction points.

connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m () Source #

Hook up meta variable to interaction point.

removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m () Source #

Mark an interaction point as solved.

getInteractionPoints :: ReadTCState m => m [InteractionId] Source #

Get a list of interaction ids.

getInteractionMetas :: ReadTCState m => m [MetaId] Source #

Get all metas that correspond to unsolved interaction ids.

getUniqueMetasRanges :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range] Source #

getUnsolvedMetas :: (MonadFail m, ReadTCState m) => m [Range] Source #

getUnsolvedInteractionMetas :: (MonadFail m, ReadTCState m) => m [Range] Source #

getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)] Source #

Get all metas that correspond to unsolved interaction ids.

isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId) Source #

Does the meta variable correspond to an interaction point?

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

lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint Source #

Get the information associated to an interaction point.

lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId Source #

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

lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId) Source #

Check whether an interaction id is already associated with a meta variable.

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId Source #

newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

Generate new meta variable.

newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source #

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

getInteractionRange :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) => InteractionId -> m Range Source #

Get the Range' for an interaction point.

getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range Source #

Get the Range' for a meta variable.

getInteractionScope :: InteractionId -> TCM ScopeInfo Source #

withMetaInfo' :: MetaVariable -> TCM a -> TCM a Source #

withMetaInfo :: Closure Range -> TCM a -> TCM a Source #

getMetaVariableSet :: ReadTCState m => m IntSet Source #

getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId] Source #

getInstantiatedMetas :: ReadTCState m => m [MetaId] Source #

getOpenMetas :: ReadTCState m => m [MetaId] Source #

isOpenMeta :: MetaInstantiation -> Bool Source #

listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

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

unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

Unregister a listener.

getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener] Source #

Get the listeners to a meta.

clearMetaListeners :: MonadMetaSolver m => MetaId -> m () Source #

Freezing and unfreezing metas.

withFreezeMetas :: TCM a -> TCM a Source #

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

freezeMetas :: TCM [MetaId] Source #

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

freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId] Source #

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

unfreezeMetas :: TCM () Source #

Thaw all meta variables.

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

Thaw some metas, as indicated by the passed condition.

isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

class UnFreezeMeta a where Source #

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

Methods

unfreezeMeta :: MonadMetaSolver m => a -> m () Source #

Instances

Instances details

UnFreezeMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #
UnFreezeMeta Level Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #
UnFreezeMeta PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source #
UnFreezeMeta Sort Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #
UnFreezeMeta Term Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Term -> m () Source #
UnFreezeMeta Type Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #
UnFreezeMeta a => UnFreezeMeta [a] Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => [a] -> m () Source #