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

Safe HaskellNone
LanguageHaskell98

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