Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
setInterface :: Interface -> TCM ()Source
curIF :: TCM InterfaceSource
curSig :: TCM SignatureSource
curMName :: TCM ModuleNameSource
curHsMod :: TCM ModuleNameSource
curDefs :: TCM DefinitionsSource
sigMName :: Signature -> ModuleNameSource
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 -> NameSource
unqhname :: String -> QName -> NameSource
tlmodOf :: ModuleName -> TCM ModuleNameSource
tlmname :: ModuleName -> TCM ModuleNameSource
xqual :: QName -> Name -> TCM QNameSource
xhqn :: String -> QName -> TCM QNameSource
conhqn :: QName -> TCM QNameSource
bltQual :: String -> String -> TCM QNameSource
hsVarUQ :: Name -> ExpSource
mazMod :: ModuleName -> ModuleNameSource
mazRTE :: ModuleNameSource
fakeD :: Name -> String -> DeclSource
fakeDS :: String -> String -> DeclSource
fakeDQ :: QName -> String -> DeclSource
fakeType :: String -> TypeSource
fakeExp :: String -> ExpSource
dummy :: aSource
gshow' :: Data a => a -> StringSource
Produced by Haddock version 2.6.1