| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Unquote
- agdaTermType :: TCM Type
- agdaTypeType :: TCM Type
- qNameType :: TCM Type
- data Dirty
- type UnquoteState = (Dirty, TCState)
- type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptionT UnquoteError TCM)))
- type UnquoteRes a = Either UnquoteError ((a, UnquoteState), [QName])
- unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
- packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
- runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
- liftU :: TCM a -> UnquoteM a
- liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b
- liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c
- inOriginalContext :: UnquoteM a -> UnquoteM a
- isCon :: ConHead -> TCM Term -> UnquoteM Bool
- isDef :: QName -> TCM Term -> UnquoteM Bool
- reduceQuotedTerm :: Term -> UnquoteM Term
- class Unquote a where
- unquoteN :: Unquote a => Arg Term -> UnquoteM a
- choice :: Monad m => [(m Bool, m a)] -> m a -> m a
- ensureDef :: QName -> UnquoteM QName
- ensureCon :: QName -> UnquoteM QName
- pickName :: Type -> String
- unquoteString :: Term -> UnquoteM String
- unquoteNString :: Arg Term -> UnquoteM String
- data ErrorPart
- getCurrentPath :: TCM AbsolutePath
- unquoteTCM :: Term -> Term -> UnquoteM Term
- evalTCM :: Term -> UnquoteM Term
Documentation
agdaTermType :: TCM Type Source #
agdaTypeType :: TCM Type Source #
type UnquoteState = (Dirty, TCState) Source #
type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptionT UnquoteError TCM))) Source #
type UnquoteRes a = Either UnquoteError ((a, UnquoteState), [QName]) Source #
unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a) Source #
packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a Source #
runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName])) Source #
liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b Source #
liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c Source #
inOriginalContext :: UnquoteM a -> UnquoteM a Source #
class Unquote a where Source #
Minimal complete definition
Instances
| Unquote Bool Source # | |
| Unquote Char Source # | |
| Unquote Double Source # | |
| Unquote Integer Source # | |
| Unquote Str Source # | |
| Unquote MetaId Source # | |
| Unquote ArgInfo Source # | |
| Unquote Relevance Source # | |
| Unquote Hiding Source # | |
| Unquote QName Source # | |
| Unquote Literal Source # | |
| Unquote Clause Source # | |
| Unquote Pattern Source # | |
| Unquote Sort Source # | |
| Unquote Term Source # | |
| Unquote Elim Source # | |
| Unquote ErrorPart Source # | |
| Unquote a => Unquote [a] Source # | |
| Unquote a => Unquote (Dom a) Source # | |
| Unquote a => Unquote (Arg a) Source # | |
| Unquote a => Unquote (Abs a) Source # | |