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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.MAlonzo.Misc

Contents

Synopsis

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.

ihname :: String -> Nat -> Name Source #

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

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

hsName :: String -> QName Source #

bltQual :: String -> String -> TCM QName 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 #

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

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

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

mazstr :: String Source #

mazMod' :: String -> ModuleName Source #

mazerror :: String -> a Source #

rtmQual :: String -> QName Source #

rtmVar :: String -> Exp Source #

rtmError :: String -> Exp 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 #

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.