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

Safe Haskell | None
Language | Haskell2010

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 #