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

• curHsMod :: TCM ModuleName
• ihname :: String -> Nat -> Name
• unqhname :: String -> QName -> Name
• tlmodOf :: ModuleName -> TCM ModuleName
• xqual :: QName -> Name -> TCM QName
• xhqn :: String -> QName -> TCM QName
• hsName :: String -> QName
• conhqn :: QName -> TCM QName
• bltQual :: String -> String -> TCM QName
• dname :: QName -> Name
• duname :: QName -> Name
• hsPrimOp :: String -> QOp
• hsPrimOpApp :: String -> Exp -> Exp -> Exp
• hsInt :: Integer -> Exp
• hsTypedInt :: Integer -> Exp
• hspLet :: Pat -> Exp -> Exp -> Exp
• hsLet :: Name -> Exp -> Exp -> Exp
• hsVarUQ :: Name -> Exp
• hsAppView :: Exp -> [Exp]
• hsOpToExp :: QOp -> Exp
• hsLambda :: [Pat] -> Exp -> Exp
• hsMapAlt :: (Exp -> Exp) -> Alt -> Alt
• hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs
• mazstr :: String
• mazName :: Name
• mazMod' :: String -> ModuleName
• mazMod :: ModuleName -> ModuleName
• mazerror :: String -> a
• mazCoerceName :: String
• mazErasedName :: String
• mazCoerce :: Exp
• mazIncompleteMatch :: Exp
• rtmIncompleteMatch :: QName -> Exp
• mazUnreachableError :: Exp
• rtmUnreachableError :: Exp
• mazRTE :: 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
• fakeDecl :: String -> Decl
• dummy :: a
• emptyBinds :: Maybe Binds

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.