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

Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Quote

Documentation

data QuotingKit Source

Constructors

QuotingKit
Fields quoteTermWithKit :: Term -> ReduceM Term quoteTypeWithKit :: Type -> ReduceM Term quoteClauseWithKit :: Clause -> ReduceM Term quoteDomWithKit :: Dom Type -> ReduceM Term

quotingKit :: TCM QuotingKit Source

quoteName :: QName -> Term Source

quoteConName :: ConHead -> Term Source

quoteTerm :: Term -> TCM Term Source

quoteType :: Type -> TCM Term Source

agdaTermType :: TCM Type Source

qNameType :: TCM Type Source

type UnquoteM = ExceptionT UnquoteError TCM Source

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

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

class Unquote a where Source

Methods

unquote :: Term -> UnquoteM a Source

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 Source

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

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

ensureDef :: QName -> UnquoteM QName Source

ensureCon :: QName -> UnquoteM QName Source

pickName :: Type -> String Source

data UnquotedFunDef Source

Constructors

UnQFun Type [Clause]

Instances

Unquote UnquotedFunDef

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