- modifyContextEntry :: (Arg (Name, Type) -> Arg (Name, Type)) -> ContextEntry -> ContextEntry
- modifyContextEntries :: (Arg (Name, Type) -> Arg (Name, Type)) -> Context -> Context
- modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a
- mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntry
- addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm a
- addContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
- addCtxString :: MonadTCM tcm => String -> Arg Type -> tcm a -> tcm a
- inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
- underAbstraction :: (Raise a, MonadTCM tcm) => Arg Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: (Raise a, 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 => Relevance -> Name -> Term -> Type -> 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
modifyContextEntry :: (Arg (Name, Type) -> Arg (Name, Type)) -> ContextEntry -> ContextEntrySource
Modify the ctxEntry
field of a ContextEntry
.
modifyContextEntries :: (Arg (Name, Type) -> Arg (Name, Type)) -> Context -> ContextSource
Modify all ContextEntry
s.
modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm aSource
Modify a Context
in a computation.
mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntrySource
addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm aSource
addCtx x arg cont
add a variable to the context.
Chooses an unused Name
.
addCtxString :: MonadTCM tcm => String -> Arg Type -> tcm a -> tcm aSource
Turns the string into a name and adds it to the context.
underAbstraction :: (Raise a, MonadTCM tcm) => Arg Type -> Abs a -> (a -> tcm b) -> tcm bSource
Go under an abstraction.
underAbstraction_ :: (Raise a, 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 => Relevance -> Name -> Term -> Type -> tcm a -> tcm aSource
Add a let bound variable
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