Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.Convert
Documentation
norm
::
Normalise
t => t ->
TCM
t
Source
type
O
= (
Maybe
Int
,
QName
)
Source
data
TMode
Source
Constructors
TMAll
type
MapS
a b = (
Map
a b, [a])
Source
data
S
Source
Constructors
S
sConsts
::
MapS
QName
(
TMode
,
ConstRef
O
)
sMetas
::
MapS
MetaId
(
Metavar
(
Exp
O
) (
RefInfo
O
),
Maybe
(
MExp
O
, [
MExp
O
]), [
MetaId
])
sEqs
::
MapS
Int
(
Maybe
(
Bool
,
MExp
O
,
MExp
O
))
sCurMeta
::
Maybe
MetaId
type
TOM
=
StateT
S
TCM
Source
tomy
::
MetaId
-> [(
Bool
,
QName
)] ->
TCM
([
ConstRef
O
],
Map
MetaId
(
Metavar
(
Exp
O
) (
RefInfo
O
),
MExp
O
, [
MExp
O
], [
MetaId
]), [(
Bool
,
MExp
O
,
MExp
O
)],
Map
QName
(
TMode
,
ConstRef
O
))
Source
getConst
::
Bool
->
QName
->
TMode
->
TOM
(
ConstRef
O
)
Source
getMeta
::
MetaId
->
TOM
(
Metavar
(
Exp
O
) (
RefInfo
O
))
Source
getEqs
::
TCM
[(
Bool
,
Term
,
Term
)]
Source
weaken
::
Int
->
MExp
O
->
MExp
O
Source
weakens
::
Int
->
MArgList
O
->
MArgList
O
Source
tomyType
::
Type
->
TOM
(
MExp
O
)
Source
tomyExp
::
Term
->
TOM
(
MExp
O
)
Source
fmType
::
MetaId
->
Type
->
Bool
Source
fmExp
::
MetaId
->
Term
->
Bool
Source
frommyExp
::
MExp
O
->
IO
Term
Source
frommyExps
::
Nat
->
MArgList
O
->
IO
Args
Source
Produced by
Haddock
version 2.6.0