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