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

Safe Haskell	None

Agda.TypeChecking.Quote

Documentation

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

quoteName :: QName -> Term Source

quoteTerm :: Term -> TCM Term Source

quoteType :: Type -> TCM Term Source

agdaTermType :: TCM Type Source

qNameType :: TCM Type Source

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

unquoteFailedGeneric :: String -> TCM aSource

unquoteFailed :: String -> String -> Term -> TCM aSource

class Unquote a whereSource

Methods

unquote :: Term -> TCM aSource

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 aSource

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

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