Agda.TypeChecking.Unquote

Documentation

agdaTermType :: TCM Type

qNameType :: TCM Type

type UnquoteM = ExceptionT UnquoteError TCM

runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError a)

isCon :: ConHead -> TCM Term -> UnquoteM Bool

class Unquote a where

Methods

unquote :: Term -> UnquoteM 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 -> UnquoteM a

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

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

ensureDef :: QName -> UnquoteM QName

ensureCon :: QName -> UnquoteM QName

pickName :: Type -> String

data UnquotedFunDef

Constructors

UnQFun Type [Clause]

Instances

Unquote UnquotedFunDef

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