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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Unquote

Synopsis

Documentation

data Dirty #

Constructors

Dirty 
Clean 

Instances

Eq Dirty # 

Methods

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

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

liftU :: TCM a -> UnquoteM a #

liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b #

liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c #

class Unquote a where #

Minimal complete definition

unquote

Methods

unquote :: Term -> UnquoteM a #

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

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

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).