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

Safe Haskell | None
Language | Haskell2010

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 :: Integral a => a -> 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
- mazAnyTypeName :: String
- mazCoerce :: Exp
- mazIncompleteMatch :: Exp
- rtmIncompleteMatch :: QName -> Exp
- mazUnreachableError :: Exp
- rtmUnreachableError :: Exp
- mazAnyType :: Type
- 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
- emptyBinds :: Maybe Binds
- isModChar :: Char -> Bool

# Documentation

curHsMod :: TCM ModuleName Source #

# 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 Source #

unqhname :: String -> QName -> Name Source #

tlmodOf :: ModuleName -> TCM ModuleName Source #

xqual :: QName -> Name -> TCM QName Source #

xhqn :: String -> QName -> TCM QName Source #

hsName :: String -> QName Source #

conhqn :: QName -> TCM QName Source #

bltQual :: String -> String -> TCM QName Source #

dname :: QName -> Name Source #

duname :: QName -> Name Source #

Name for definition stripped of unused arguments

hsPrimOp :: String -> QOp Source #

hsPrimOpApp :: String -> Exp -> Exp -> Exp Source #

hsInt :: Integer -> Exp Source #

hsTypedInt :: Integral a => a -> Exp Source #

hsLet :: Name -> Exp -> Exp -> Exp Source #

hsVarUQ :: Name -> Exp Source #

hsAppView :: Exp -> [Exp] Source #

hsOpToExp :: QOp -> Exp Source #

hsLambda :: [Pat] -> Exp -> Exp Source #

hsMapAlt :: (Exp -> Exp) -> Alt -> Alt Source #

hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs Source #

mazstr :: String Source #

mazName :: Name Source #

mazMod' :: String -> ModuleName Source #

mazMod :: ModuleName -> ModuleName Source #

mazerror :: String -> a Source #

mazCoerceName :: String Source #

mazErasedName :: String Source #

mazAnyTypeName :: String Source #

mazCoerce :: Exp Source #

mazIncompleteMatch :: Exp Source #

rtmIncompleteMatch :: QName -> Exp Source #

mazUnreachableError :: Exp Source #

rtmUnreachableError :: Exp Source #

mazAnyType :: Type Source #

mazRTE :: ModuleName Source #

rtmQual :: String -> QName Source #

rtmVar :: String -> Exp Source #

rtmError :: String -> Exp Source #

unsafeCoerceMod :: ModuleName Source #

fakeD :: Name -> String -> Decl Source #

fakeDS :: String -> String -> Decl Source #

fakeDQ :: QName -> String -> Decl Source #

fakeType :: String -> Type Source #

fakeExp :: String -> Exp Source #

fakeDecl :: String -> Decl Source #

emptyBinds :: Maybe Binds Source #

isModChar :: Char -> Bool Source #

Can the character be used in a Haskell module name part (`conid`)? This function is more restrictive than what the Haskell report allows.