Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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
setInterface
::
Interface
->
TCM
()
curIF
::
TCM
Interface
curSig
::
TCM
Signature
curMName
::
TCM
ModuleName
curHsMod
::
TCM
ModuleName
curDefs
::
TCM
Definitions
sigMName
::
Signature
->
ModuleName
ihname
::
String
->
Nat
->
Name
unqhname
::
String
->
QName
->
Name
tlmodOf
::
ModuleName
->
TCM
ModuleName
tlmname
::
ModuleName
->
TCM
ModuleName
xqual
::
QName
->
Name
->
TCM
QName
xhqn
::
String
->
QName
->
TCM
QName
conhqn
::
QName
->
TCM
QName
bltQual
::
String
->
String
->
TCM
QName
hsVarUQ
::
Name
->
Exp
mazMod
::
ModuleName
->
ModuleName
mazRTE
::
ModuleName
fakeD
::
Name
->
String
->
Decl
fakeDS
::
String
->
String
->
Decl
fakeDQ
::
QName
->
String
->
Decl
fakeType
::
String
->
Type
fakeExp
::
String
->
Exp
dummy
:: a
gshow'
::
Data
a => a ->
String
Documentation
setInterface
::
Interface
->
TCM
()
Source
curIF
::
TCM
Interface
Source
curSig
::
TCM
Signature
Source
curMName
::
TCM
ModuleName
Source
curHsMod
::
TCM
ModuleName
Source
curDefs
::
TCM
Definitions
Source
sigMName
::
Signature
->
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
tlmname
::
ModuleName
->
TCM
ModuleName
Source
xqual
::
QName
->
Name
->
TCM
QName
Source
xhqn
::
String
->
QName
->
TCM
QName
Source
conhqn
::
QName
->
TCM
QName
Source
bltQual
::
String
->
String
->
TCM
QName
Source
hsVarUQ
::
Name
->
Exp
Source
mazMod
::
ModuleName
->
ModuleName
Source
mazRTE
::
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
dummy
:: a
Source
gshow'
::
Data
a => a ->
String
Source
Produced by
Haddock
version 2.6.1