Agda-2.5.2: 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.

duname :: QName -> Name #

Name for definition stripped of unused arguments

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

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

hsAppView :: Exp -> [Exp] #

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

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

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

mazerror :: String -> a #

isModChar :: Char -> Bool #

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