Agda-2.5.1: 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
 
quoteDefnWithKit :: Definition -> ReduceM Term
 
quoteListWithKit :: forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
 

quotingKit :: TCM QuotingKit Source

quoteString :: String -> Term Source

quoteName :: QName -> Term Source

quoteNat :: Integer -> Term Source

quoteConName :: ConHead -> Term Source

quoteMeta :: AbsolutePath -> MetaId -> Term Source

quoteTerm :: Term -> TCM Term Source

quoteType :: Type -> TCM Term Source

quoteDom :: Dom Type -> TCM Term Source

quoteDefn :: Definition -> TCM Term Source

quoteList :: [Term] -> TCM Term Source