Agda.TypeChecking.Quote

Documentation

data QuotingKit

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

quoteString :: String -> Term

quoteName :: QName -> Term

quoteNat :: Integer -> Term

quoteConName :: ConHead -> Term

quoteMeta :: AbsolutePath -> MetaId -> Term

quoteTerm :: Term -> TCM Term

quoteType :: Type -> TCM Term

quoteDom :: Dom Type -> TCM Term

quoteDefn :: Definition -> TCM Term

quoteList :: [Term] -> TCM Term