Agda.Compiler.MAlonzo.Misc

Documentation

curHsMod :: TCM ModuleName

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.

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

Name for definition stripped of unused arguments

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 :: Binds