Agda.Compiler.MAlonzo.Misc

Contents

• 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.

Synopsis

• 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
• hsVarUQ :: Name -> Exp
• mazMod :: ModuleName -> ModuleName
• mazRTE :: ModuleName
• fakeD :: Name -> String -> Decl
• fakeDS :: String -> String -> Decl
• fakeDQ :: QName -> String -> Decl
• fakeType :: String -> Type
• fakeExp :: String -> Exp
• dummy :: a
• gshow' :: Data a => a -> String

Documentation

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.