- setInterface :: Interface -> TCM ()
- curIF :: TCM Interface
- curSig :: TCM Signature
- curMName :: TCM ModuleName
- curHsMod :: TCM Module
- curDefs :: TCM Definitions
- sigMName :: Signature -> ModuleName
- ihname :: String -> Nat -> HsName
- unqhname :: String -> QName -> HsName
- tlmodOf :: ModuleName -> TCM Module
- tlmname :: ModuleName -> TCM ModuleName
- xqual :: QName -> HsName -> TCM HsQName
- xhqn :: String -> QName -> TCM HsQName
- conhqn :: QName -> TCM HsQName
- bltQual :: String -> String -> TCM HsQName
- hsVarUQ :: HsName -> HsExp
- mazMod :: ModuleName -> Module
- fakeD :: HsName -> String -> HsDecl
- fakeDS :: String -> String -> HsDecl
- fakeDQ :: QName -> String -> HsDecl
- fakeType :: String -> HsQualType
- fakeExp :: String -> HsExp
- dummy :: a
- gshow' :: Data a => a -> String
Documentation
setInterface :: Interface -> TCM ()Source
Types coming from Agda are named T<number>.
Other definitions coming from Agda are named d<number>.
Names coming from Haskell must always be used qualified.
tlmodOf :: ModuleName -> TCM ModuleSource
tlmname :: ModuleName -> TCM ModuleNameSource
mazMod :: ModuleName -> ModuleSource
fakeType :: String -> HsQualTypeSource