Agda.TypeChecking.Quote

Documentation

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

quoteName :: QName -> Term

quoteConName :: ConHead -> Term

quoteTerm :: Term -> TCM Term

quoteType :: Type -> TCM Term

agdaTermType :: TCM Type

qNameType :: TCM Type

isCon :: ConHead -> 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 Char

Unquote Double

Unquote Integer

Unquote Str

Unquote Relevance

Unquote Hiding

Unquote QName

Unquote Literal

Unquote Pattern

Unquote Clause

Unquote Level

Unquote Sort

Unquote Type

Unquote Term

Unquote ConHead

Unquote ArgInfo

Unquote UnquotedFunDef

Unquote a => Unquote [a]

Unquote a => Unquote (Abs a)

Unquote a => Unquote (Elim' a)

Unquote a => Unquote (Arg 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

ensureDef :: QName -> TCM QName

ensureCon :: QName -> TCM QName

pickName :: Type -> String

data UnquotedFunDef

Constructors

UnQFun Type [Clause]

Instances

Unquote UnquotedFunDef

reifyUnquoted :: Reify a e => a -> TCM e