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

Safe Haskell | Safe-Inferred
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

- 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 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 #