| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Compiler.MAlonzo.Misc
Contents
- setInterface :: Interface -> TCM ()
- curIF :: TCM Interface
- curSig :: TCM Signature
- curMName :: TCM ModuleName
- curHsMod :: TCM ModuleName
- curDefs :: TCM Definitions
- sigMName :: Signature -> ModuleName
- ihname :: String -> Nat -> Name
- unqhname :: String -> QName -> Name
- tlmodOf :: ModuleName -> TCM ModuleName
- tlmname :: ModuleName -> TCM ModuleName
- xqual :: QName -> Name -> TCM QName
- xhqn :: String -> QName -> TCM QName
- conhqn :: QName -> TCM QName
- bltQual :: String -> String -> TCM QName
- dsubname :: QName -> Nat -> Name
- hsVarUQ :: Name -> Exp
- mazstr :: String
- mazName :: Name
- mazMod' :: String -> ModuleName
- mazMod :: ModuleName -> ModuleName
- mazerror :: String -> a
- mazCoerce :: Exp
- mazIncompleteMatch :: Exp
- rtmIncompleteMatch :: QName -> Exp
- mazRTE :: ModuleName
- rtmMod :: ModuleName
- rtmQual :: String -> QName
- rtmVar :: String -> Exp
- rtmError :: String -> Exp
- unsafeCoerceMod :: ModuleName
- fakeD :: Name -> String -> Decl
- fakeDS :: String -> String -> Decl
- fakeDQ :: QName -> String -> Decl
- fakeType :: String -> Type
- fakeExp :: String -> Exp
- dummy :: a
Documentation
setInterface :: Interface -> TCM () Source
sigMName :: Signature -> ModuleName 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 ModuleName Source
tlmname :: ModuleName -> TCM ModuleName Source
mazMod :: ModuleName -> ModuleName Source
mazIncompleteMatch :: Exp Source
rtmIncompleteMatch :: QName -> Exp Source
unsafeCoerceMod :: ModuleName Source