ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Quote

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

Parse quote.

datadata QuotingKit

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