Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.Typecheck
Documentation
tcExp
::
Bool
->
Ctx
o ->
CExp
o ->
MExp
o ->
EE
(
MyPB
o)
Source
getDatatype
::
ICExp
o ->
EE
(
MyMB
(
Maybe
(
ICArgList
o, [
ConstRef
o])) o)
Source
constructorImpossible
::
ICArgList
o ->
ConstRef
o ->
EE
(
MyPB
o)
Source
unequals
::
ICArgList
o ->
ICArgList
o -> ([(
Nat
,
HNExp
o)] ->
EE
(
MyPB
o)) -> [(
Nat
,
HNExp
o)] ->
EE
(
MyPB
o)
Source
unequal
::
ICExp
o ->
ICExp
o -> ([(
Nat
,
HNExp
o)] ->
EE
(
MyPB
o)) -> [(
Nat
,
HNExp
o)] ->
EE
(
MyPB
o)
Source
traversePi
::
Int
->
ICExp
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
tcargs
::
Nat
->
Bool
->
Ctx
o ->
CExp
o ->
MArgList
o ->
MExp
o ->
Bool
-> (
CExp
o ->
MExp
o ->
EE
(
MyPB
o)) ->
EE
(
MyPB
o)
Source
type
HNNBlks
o = [
HNExp
o]
Source
hnn
::
ICExp
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
hnn_blks
::
ICExp
o ->
EE
(
MyMB
(
HNExp
o,
HNNBlks
o) o)
Source
hnn_checkstep
::
ICExp
o ->
EE
(
MyMB
(
HNExp
o,
Bool
) o)
Source
hnn'
::
ICExp
o ->
ICArgList
o ->
EE
(
MyMB
(
HNExp
o,
HNNBlks
o) o)
Source
hnb
::
ICExp
o ->
ICArgList
o ->
EE
(
MyMB
(
HNExp
o) o)
Source
data
HNRes
o
Source
Constructors
HNDone
(
Maybe
(
Metavar
(
Exp
o) (
RefInfo
o))) (
HNExp
o)
HNMeta
(
ICExp
o) (
ICArgList
o) [
Maybe
(
UId
o)]
hnc
::
Bool
->
ICExp
o ->
ICArgList
o -> [
Maybe
(
UId
o)] ->
EE
(
MyMB
(
HNRes
o) o)
Source
hnarglist
::
ICArgList
o ->
EE
(
MyMB
(
HNArgList
o) o)
Source
getNArgs
::
Nat
->
ICArgList
o ->
EE
(
MyMB
(
Maybe
([
ICExp
o],
ICArgList
o)) o)
Source
getAllArgs
::
ICArgList
o ->
EE
(
MyMB
[
ICExp
o] o)
Source
data
PEval
o
Source
Constructors
PENo
(
ICExp
o)
PEConApp
(
ICExp
o) (
ConstRef
o) [
PEval
o]
iotastep
::
Bool
->
HNExp
o ->
EE
(
MyMB
(
Either
(
ICExp
o,
ICArgList
o) (
HNNBlks
o)) o)
Source
noiotastep
::
HNExp
o ->
EE
(
MyPB
o)
Source
noiotastep_term
::
ConstRef
o ->
MArgList
o ->
EE
(
MyPB
o)
Source
data
CMode
o
Source
Constructors
CMRigid
(
Maybe
(
Metavar
(
Exp
o) (
RefInfo
o))) (
HNExp
o)
forall
b .
Refinable
b (
RefInfo
o) =>
CMFlex
(
MM
b (
RefInfo
o)) (
CMFlex
o)
data
CMFlex
o
Source
Constructors
CMFFlex
(
ICExp
o) (
ICArgList
o) [
Maybe
(
UId
o)]
CMFSemi
(
Maybe
(
Metavar
(
Exp
o) (
RefInfo
o))) (
HNExp
o)
CMFBlocked
(
Maybe
(
Metavar
(
Exp
o) (
RefInfo
o))) (
HNExp
o)
comp'
::
forall
o.
Bool
->
CExp
o ->
CExp
o ->
EE
(
MyPB
o)
Source
checkeliminand
::
MExp
o ->
EE
(
MyPB
o)
Source
iotapossmeta
::
ICExp
o ->
ICArgList
o ->
EE
Bool
Source
meta_not_constructor
::
ICExp
o ->
EE
(
MB
Bool
(
RefInfo
o))
Source
calcEqRState
::
EqReasoningConsts
o ->
MExp
o ->
EE
(
MyPB
o)
Source
pickid
::
MId
->
MId
->
MId
Source
tcSearch
::
Bool
->
Ctx
o ->
CExp
o ->
MExp
o ->
EE
(
MyPB
o)
Source
Produced by
Haddock
version 2.6.1