Agda-2.4.0.2: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Quote
quotingKit :: TCM (Term -> Term, Type -> Term) Source
quoteName :: QName -> Term Source
quoteConName :: ConHead -> Term Source
quoteTerm :: Term -> TCM Term Source
quoteType :: Type -> TCM Term Source
agdaTermType :: TCM Type Source
qNameType :: TCM Type Source
isCon :: ConHead -> TCM Term -> TCM Bool Source
unquoteFailedGeneric :: String -> TCM a Source
unquoteFailed :: String -> String -> Term -> TCM a Source
class Unquote a where Source
Methods
unquote :: Term -> TCM a Source
Instances
unquoteH :: Unquote a => Arg Term -> TCM a Source
unquoteN :: Unquote a => Arg Term -> TCM a Source
choice :: Monad m => [(m Bool, m a)] -> m a -> m a Source