Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.MAlonzo.Compiler
Synopsis
compilerMain :: Interface -> TCM ()
compile :: Interface -> TCM ()
imports :: TCM [HsImportDecl]
definitions :: Definitions -> TCM [HsDecl]
definition :: Definition -> TCM [HsDecl]
checkConstructorType :: QName -> TCM [HsDecl]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HsDecl]
constructorArity :: MonadTCM tcm => QName -> tcm Nat
clause :: QName -> (Nat, Bool, Clause) -> TCM HsDecl
argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat]
clausebody :: ClauseBody -> TCM HsExp
term :: Term -> ReaderT Nat TCM HsExp
literal :: Literal -> TCM HsExp
hslit :: Literal -> HsLiteral
condecl :: QName -> TCM (Nat, HsConDecl)
cdecl :: QName -> Nat -> HsConDecl
tvaldecl :: QName -> Induction -> Nat -> Nat -> [HsConDecl] -> Maybe Clause -> [HsDecl]
infodecl :: QName -> HsDecl
hsCast :: HsExp -> HsExp
writeModule :: HsModule -> TCM ()
malonzoDir :: TCM FilePath
outFile :: TCM FilePath
callGHC :: Interface -> TCM ()
Documentation
compilerMain :: Interface -> TCM ()Source
compile :: Interface -> TCM ()Source
imports :: TCM [HsImportDecl]Source
definitions :: Definitions -> TCM [HsDecl]Source
definition :: Definition -> TCM [HsDecl]Source
checkConstructorType :: QName -> TCM [HsDecl]Source
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HsDecl]Source
constructorArity :: MonadTCM tcm => QName -> tcm NatSource
Move somewhere else!
clause :: QName -> (Nat, Bool, Clause) -> TCM HsDeclSource
argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat]Source
clausebody :: ClauseBody -> TCM HsExpSource
term :: Term -> ReaderT Nat TCM HsExpSource
literal :: Literal -> TCM HsExpSource
hslit :: Literal -> HsLiteralSource
condecl :: QName -> TCM (Nat, HsConDecl)Source
cdecl :: QName -> Nat -> HsConDeclSource
tvaldeclSource
:: QName
-> InductionIs the type inductive or coinductive?
-> Nat
-> Nat
-> [HsConDecl]
-> Maybe Clause
-> [HsDecl]
infodecl :: QName -> HsDeclSource
hsCast :: HsExp -> HsExpSource
writeModule :: HsModule -> TCM ()Source
malonzoDir :: TCM FilePathSource
outFile :: TCM FilePathSource
callGHC :: Interface -> TCM ()Source
Produced by Haddock version 2.6.0