Agda-2.6.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 #