Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Quote

Synopsis

value quotedName
data QuotingKit
value quotingKit
value quoteString
value quoteName
value quoteNat
value quoteConName
value quoteMeta
value quoteTerm
value quoteType
value quoteDom
value quoteDefn
value quoteList

PackageAgda-2.8.0.2
Exports13
LanguageHaskell2010
LicenceMIT
SourceQuote.hs

valuequotedName :: (MonadTCError m, MonadAbsToCon m) => Expr -> m QName

Parse quote.

datadata QuotingKit

Constructors

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

valuequotingKit :: TCM QuotingKit

valuequoteString :: String -> Term

valuequoteName :: QName -> Term

valuequoteNat :: Integer -> Term

valuequoteConName :: ConHead -> Term

valuequoteMeta :: TopLevelModuleName -> MetaId -> Term

valuequoteTerm :: Term -> TCM Term

valuequoteType :: Type -> TCM Term

valuequoteDom :: Dom Type -> TCM Term

valuequoteDefn :: Definition -> TCM Term

valuequoteList :: [Term] -> TCM Term