| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Quote
Synopsis
- quotedName :: (MonadTCError m, MonadAbsToCon m) => Expr -> m QName
- data QuotingKit = QuotingKit {
- quoteTermWithKit :: Term -> ReduceM Term
- quoteTypeWithKit :: Type -> 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
Documentation
quotedName :: (MonadTCError m, MonadAbsToCon m) => Expr -> m QName Source #
Parse quote.
data QuotingKit Source #
Constructors
| QuotingKit | |
Fields
| |
quoteString :: String -> Term Source #
quoteConName :: ConHead -> Term Source #