Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Quote

# Documentation

quotingKit :: TCM (Term -> Term, Type -> Term)

quoteName :: QName -> Term

quoteTerm :: Term -> TCM Term

quoteType :: Type -> TCM Term

agdaTermType :: TCM Type

qNameType :: TCM Type

isCon :: QName -> TCM Term -> TCM Bool

unquoteFailedGeneric :: String -> TCM a

unquoteFailed :: String -> String -> Term -> TCM a

class Unquote a where

Methods

unquote :: Term -> TCM a

Instances

Unquote Integer |
Unquote Relevance |
Unquote Hiding |
Unquote QName |
Unquote Level |
Unquote Sort |
Unquote Type |
Unquote Term |
Unquote a => Unquote [a] |
Unquote a => Unquote (Arg a) |
Unquote a => Unquote (Abs a) |

unquoteH :: Unquote a => Arg Term -> TCM a

unquoteN :: Unquote a => Arg Term -> TCM a

choice :: Monad m => [(m Bool, m a)] -> m a -> m a