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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Unquote

Synopsis

Documentation

data Dirty Source #

Constructors

Dirty 
Clean 
Instances
Eq Dirty Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

(==) :: Dirty -> Dirty -> Bool #

(/=) :: Dirty -> Dirty -> Bool #

class Unquote a where Source #

Minimal complete definition

unquote

Methods

unquote :: Term -> UnquoteM a Source #

Instances
Unquote Bool Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Char Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Double Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Integer Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Str Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Literal Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Clause Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Sort Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Term Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote a => Unquote [a] Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM [a] Source #

Unquote a => Unquote (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

Unquote a => Unquote (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a) Source #

Unquote a => Unquote (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a) Source #

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

unquoteTCM :: Term -> Term -> UnquoteM Term Source #

Argument should be a term of type Term → TCM A for some A. Returns the resulting term of type A. The second argument is the term for the hole, which will typically be a metavariable. This is passed to the computation (quoted).