Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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
- dsubname :: (Eq a, Num a, Show a) => QName -> a -> Name
- hsVarUQ :: Name -> Exp
- mazstr :: [Char]
- mazName :: Name
- mazMod' :: [Char] -> ModuleName
- mazMod :: ModuleName -> ModuleName
- mazerror :: [Char] -> t
- mazCoerce :: Exp
- mazIncompleteMatch :: Exp
- rtmIncompleteMatch :: QName -> Exp
- mazRTE :: ModuleName
- rtmMod :: ModuleName
- rtmQual :: String -> QName
- rtmVar :: String -> Exp
- rtmError :: [Char] -> 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 ()

curIF :: TCM Interface

curSig :: TCM Signature

curMName :: TCM ModuleName

curHsMod :: TCM ModuleName

curDefs :: TCM Definitions

sigMName :: Signature -> 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

tlmname :: ModuleName -> TCM ModuleName

xqual :: QName -> Name -> TCM QName

xhqn :: String -> QName -> TCM QName

conhqn :: QName -> TCM QName

bltQual :: String -> String -> TCM QName

dsubname :: (Eq a, Num a, Show a) => QName -> a -> Name

hsVarUQ :: Name -> Exp

mazstr :: [Char]

mazName :: Name

mazMod' :: [Char] -> ModuleName

mazMod :: ModuleName -> ModuleName

mazerror :: [Char] -> t

mazCoerce :: Exp

mazIncompleteMatch :: Exp

rtmIncompleteMatch :: QName -> Exp

mazRTE :: ModuleName

rtmMod :: ModuleName

rtmQual :: String -> QName

rtmVar :: String -> Exp

rtmError :: [Char] -> Exp

unsafeCoerceMod :: ModuleName

fakeD :: Name -> String -> Decl

fakeDS :: String -> String -> Decl

fakeDQ :: QName -> String -> Decl

fakeType :: String -> Type

fakeExp :: String -> Exp

dummy :: a