Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.Typecheck
Documentation
closify
:: a ->
Clos
a o
Source
sub
::
CExp
o ->
Clos
a o ->
Clos
a o
Source
msubs
:: [
CExp
o] -> a ->
Clos
a o
Source
weak
::
Nat
->
Clos
a o ->
Clos
a o
Source
tcExp
::
Bool
->
Ctx
o ->
CExp
o ->
MExp
o ->
EE
(
MyPB
o)
Source
tcargs
::
Bool
->
Ctx
o ->
CExp
o ->
CExp
o ->
MArgList
o ->
EE
(
MyPB
o)
Source
hnn
::
CExp
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
hnn'
::
CExp
o ->
CArgList
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
hn'
::
CExp
o ->
CArgList
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
data
HNRes
o
Source
Constructors
HNDone
(
HNExp
o)
HNMeta
(
CExp
o) (
CArgList
o)
hnc
::
Bool
->
CExp
o ->
CArgList
o ->
EE
(
MyMB
(
HNRes
o) o)
Source
doclos
:: [
CAction
o] ->
Nat
->
Either
Nat
(
CExp
o)
Source
hnarglist
::
CArgList
o ->
EE
(
MyMB
(
HNArgList
o) o)
Source
getNArgs
::
Nat
->
CArgList
o ->
EE
(
MyMB
(
Maybe
([
CExp
o],
CArgList
o)) o)
Source
getAllArgs
::
CArgList
o ->
EE
(
MyMB
[
PEval
o] o)
Source
iotastep
::
HNExp
o ->
EE
(
MyMB
(
Maybe
(
CExp
o,
CArgList
o)) o)
Source
data
PEval
o
Source
Constructors
PENo
(
CExp
o)
PEConApp
(
CExp
o) (
ConstRef
o) [
PEval
o]
PEConPar
dorules
:: [
Clause
o] -> [
PEval
o] ->
EE
(
MyMB
(
Maybe
(
CExp
o)) o)
Source
dorule
::
Clause
o -> [
PEval
o] ->
EE
(
MyMB
(
Either
(
Maybe
[
PEval
o]) (
CExp
o)) o)
Source
dopats
:: [
Pat
o] -> [
PEval
o] ->
EE
(
MyMB
(
Either
(
Maybe
[
PEval
o]) ([
PEval
o], [
CExp
o])) o)
Source
dopat
::
Pat
o ->
PEval
o ->
EE
(
MyMB
(
Either
(
Maybe
(
PEval
o)) (
PEval
o, [
CExp
o])) o)
Source
noiotastep
::
HNExp
o ->
EE
(
MyPB
o)
Source
noiotastep'
::
ConstRef
o ->
MArgList
o ->
EE
(
MyPB
o)
Source
comp'
::
CExp
o ->
CExp
o ->
EE
(
MyPB
o)
Source
comp
::
Bool
->
CExp
o ->
CExp
o ->
EE
(
MyPB
o)
Source
comphn'
::
Bool
->
HNExp
o ->
HNExp
o ->
EE
(
MyPB
o)
Source
compargs
::
CArgList
o ->
CArgList
o ->
EE
(
MyPB
o)
Source
pickid
::
MId
->
MId
->
MId
Source
tcSearch
::
Ctx
o ->
CExp
o ->
MExp
o ->
EE
(
MyPB
o)
Source
ptcTypeUnknown
::
Bool
->
Ctx
o ->
CExp
o ->
MExp
o ->
EE
String
Source
ptcTypeCheck
::
Bool
->
Ctx
o ->
HNExp
o ->
MExp
o ->
EE
String
Source
ptcTypecheckArgList
::
String
->
Bool
->
Ctx
o ->
CExp
o ->
CExp
o ->
MArgList
o ->
EE
String
Source
ptcNoIotaStep
::
HNExp
o ->
EE
String
Source
ptcCompare
::
String
->
Bool
->
CExp
o ->
CExp
o ->
EE
String
Source
ptcCompareArgList
::
String
->
CArgList
o ->
CArgList
o ->
EE
String
Source
phnexp
::
Bool
->
Int
-> [
MId
] ->
HNExp
o ->
IO
String
Source
phnargs
::
Bool
-> [
MId
] ->
HNArgList
o ->
IO
String
Source
pcexp
::
Bool
->
Int
-> [
MId
] ->
CExp
o ->
IO
String
Source
pcargs
::
Bool
-> [
MId
] ->
CArgList
o ->
IO
String
Source
printCtx
::
Bool
->
Ctx
o ->
IO
String
Source
Produced by
Haddock
version 2.6.0