- findIdx :: Eq a => [a] -> a -> Maybe Int
- isBlockedTerm :: MonadTCM tcm => MetaId -> tcm Bool
- class HasMeta t where
- metaInstance :: MonadTCM tcm => t -> tcm MetaInstantiation
- metaVariable :: MetaId -> Args -> t
- (=:=) :: MonadTCM tcm => MetaId -> Term -> tcm ()
- (=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()
- assignTerm :: MonadTCM tcm => MetaId -> Term -> tcm ()
- assignSort :: MonadTCM tcm => MetaId -> Sort -> tcm ()
- newSortMeta :: MonadTCM tcm => tcm Sort
- newSortMetaCtx :: MonadTCM tcm => Args -> tcm Sort
- newTypeMeta :: MonadTCM tcm => Sort -> tcm Type
- newTypeMeta_ :: MonadTCM tcm => tcm Type
- newValueMeta :: MonadTCM tcm => Type -> tcm Term
- newValueMetaCtx :: MonadTCM tcm => Type -> Args -> tcm Term
- newValueMeta' :: MonadTCM tcm => Type -> tcm Term
- newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm Term
- newTelMeta :: MonadTCM tcm => Telescope -> tcm Args
- newArgsMeta :: MonadTCM tcm => Type -> tcm Args
- newArgsMetaCtx :: MonadTCM tcm => Type -> Telescope -> Args -> tcm Args
- newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm Term
- newRecordMetaCtx :: MonadTCM tcm => QName -> Args -> Telescope -> Args -> tcm Term
- newQuestionMark :: MonadTCM tcm => Type -> tcm Term
- blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm Term
- postponeTypeCheckingProblem_ :: MonadTCM tcm => Expr -> Type -> tcm Term
- postponeTypeCheckingProblem :: MonadTCM tcm => Expr -> Type -> TCM Bool -> tcm Term
- etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()
- etaExpandMeta :: MonadTCM tcm => MetaId -> tcm ()
- abortAssign :: MonadTCM tcm => tcm a
- handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm a
- assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm Constraints
- assignS :: MonadTCM tcm => MetaId -> Args -> Sort -> tcm Constraints
- checkArgs :: MonadTCM tcm => MetaId -> Args -> tcm [Arg Nat]
- validParameters :: Monad m => Args -> m [Arg Nat]
- isVar :: Arg Term -> Bool
- updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm ()
Documentation
findIdx :: Eq a => [a] -> a -> Maybe IntSource
Find position of a value in a list. Used to change metavar argument indices during assignment.
reverse
is necessary because we are directly abstracting over the list.
isBlockedTerm :: MonadTCM tcm => MetaId -> tcm BoolSource
Check whether a meta variable is a place holder for a blocked term.
metaInstance :: MonadTCM tcm => t -> tcm MetaInstantiationSource
metaVariable :: MetaId -> Args -> tSource
(=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()Source
The instantiation should not be an InstV
or InstS
and the MetaId
should point to something Open
or a BlockedConst
.
newSortMeta :: MonadTCM tcm => tcm SortSource
newSortMetaCtx :: MonadTCM tcm => Args -> tcm SortSource
newTypeMeta :: MonadTCM tcm => Sort -> tcm TypeSource
newTypeMeta_ :: MonadTCM tcm => tcm TypeSource
newValueMeta :: MonadTCM tcm => Type -> tcm TermSource
Create a new metavariable, possibly -expanding in the process.
newValueMeta' :: MonadTCM tcm => Type -> tcm TermSource
Create a new value meta without -expanding.
newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm TermSource
Create a new value meta with specific dependencies.
newTelMeta :: MonadTCM tcm => Telescope -> tcm ArgsSource
newArgsMeta :: MonadTCM tcm => Type -> tcm ArgsSource
newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm TermSource
Create a metavariable of record type. This is actually one metavariable for each field.
newQuestionMark :: MonadTCM tcm => Type -> tcm TermSource
blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm TermSource
Construct a blocked constant if there are constraints.
etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()Source
Eta expand metavariables listening on the current meta.
etaExpandMeta :: MonadTCM tcm => MetaId -> tcm ()Source
Eta expand a metavariable.
abortAssign :: MonadTCM tcm => tcm aSource
handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm aSource
assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm ConstraintsSource
Assign to an open metavar. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.
checkArgs :: MonadTCM tcm => MetaId -> Args -> tcm [Arg Nat]Source
Check that arguments to a metavar are in pattern fragment.
Assumes all arguments already in whnf.
Parameters are represented as Var
s so checkArgs
really
checks that all args are unique Var
s and returns the
list of corresponding indices for each arg-- done
to not define equality on Term
.
reverse
is necessary because we are directly abstracting over this list ids
.