Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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
Nat
Source
Move somewhere else!
clause
::
QName
-> (
Nat
,
Bool
,
Clause
) ->
TCM
HsDecl
Source
argpatts
:: [
Arg
Pattern
] -> [
HsPat
] ->
TCM
[
HsPat
]
Source
clausebody
::
ClauseBody
->
TCM
HsExp
Source
term
::
Term
->
ReaderT
Nat
TCM
HsExp
Source
literal
::
Literal
->
TCM
HsExp
Source
hslit
::
Literal
->
HsLiteral
Source
condecl
::
QName
->
TCM
(
Nat
,
HsConDecl
)
Source
cdecl
::
QName
->
Nat
->
HsConDecl
Source
tvaldecl
Source
::
QName
->
Induction
Is the type inductive or coinductive?
->
Nat
->
Nat
-> [
HsConDecl
]
->
Maybe
Clause
-> [
HsDecl
]
infodecl
::
QName
->
HsDecl
Source
hsCast
::
HsExp
->
HsExp
Source
writeModule
::
HsModule
->
TCM
()
Source
malonzoDir
::
TCM
FilePath
Source
outFile
::
TCM
FilePath
Source
callGHC
::
Interface
->
TCM
()
Source
Produced by
Haddock
version 2.4.2