- mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntry
- addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm a
- inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
- underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm b
- addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a
- getContext :: MonadTCM tcm => tcm [Arg (Name, Type)]
- getContextArgs :: MonadTCM tcm => tcm Args
- getContextTerms :: MonadTCM tcm => tcm [Term]
- getContextTelescope :: MonadTCM tcm => tcm Telescope
- addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm a
- getContextId :: MonadTCM tcm => tcm [CtxId]
- addLetBinding :: MonadTCM tcm => Name -> Term -> Type -> tcm a -> tcm a
- wakeIrrelevantVars :: MonadTCM tcm => tcm a -> tcm a
- applyRelevanceToContext :: MonadTCM tcm => Relevance -> tcm a -> tcm a
- typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)
- typeOfBV :: MonadTCM tcm => Nat -> tcm Type
- nameOfBV :: MonadTCM tcm => Nat -> tcm Name
- getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)
- escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
Documentation
mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntrySource
underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm bSource
Go under an abstraction.
underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm bSource
Go under an abstract without worrying about the type to add to the context.
getContextArgs :: MonadTCM tcm => tcm ArgsSource
Generate [Var n - 1, .., Var 0] for all declarations in the context.
getContextTerms :: MonadTCM tcm => tcm [Term]Source
getContextTelescope :: MonadTCM tcm => tcm TelescopeSource
addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm aSource
add a bunch of variables with the same type to the context
getContextId :: MonadTCM tcm => tcm [CtxId]Source
Check if we are in a compatible context, i.e. an extension of the given context.
addLetBinding :: MonadTCM tcm => Name -> Term -> Type -> tcm a -> tcm aSource
Add a let bound variable
wakeIrrelevantVars :: MonadTCM tcm => tcm a -> tcm aSource
Wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
applyRelevanceToContext :: MonadTCM tcm => Relevance -> tcm a -> tcm aSource
typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)Source
get type of bound variable (i.e. deBruijn index)
getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)Source
TODO: move(?)
Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm aSource