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

Safe Haskell	None
Language	Haskell2010

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 #