Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.Syntax
Documentation
type
UId
o =
Metavar
(
Exp
o) (
RefInfo
o)
Source
data
HintMode
Source
Constructors
HMNormal
HMRecCall
data
EqReasoningConsts
o
Source
Constructors
EqReasoningConsts
eqrcId
::
ConstRef
o
eqrcBegin
::
ConstRef
o
eqrcStep
::
ConstRef
o
eqrcEnd
::
ConstRef
o
eqrcSym
::
ConstRef
o
eqrcCong
::
ConstRef
o
data
EqReasoningState
Source
Constructors
EqRSNone
EqRSChain
EqRSPrf1
EqRSPrf2
EqRSPrf3
data
RefInfo
o
Source
Constructors
RIEnv
rieHints
:: [(
ConstRef
o,
HintMode
)]
rieDefFreeVars
::
Nat
rieEqReasoningConsts
::
Maybe
(
EqReasoningConsts
o)
RIMainInfo
Nat
(
HNExp
o)
Bool
forall
a .
RIUnifInfo
[
CAction
o] (
HNExp
o)
RICopyInfo
(
ICExp
o)
RIIotaStep
Bool
RIInferredTypeUnknown
RINotConstructor
RIUsedVars
[
UId
o] [
Elr
o]
RIPickSubsvar
RIEqRState
EqReasoningState
RICheckElim
Bool
RICheckProjIndex
[
ConstRef
o]
type
MyPB
o =
PB
(
RefInfo
o)
Source
type
MyMB
a o =
MB
a (
RefInfo
o)
Source
type
Nat
=
Int
Source
data
FMode
Source
Constructors
Hidden
NotHidden
data
MId
Source
Constructors
Id
String
NoId
data
Abs
a
Source
Constructors
Abs
MId
a
data
ConstDef
o
Source
Constructors
ConstDef
cdname
::
String
cdorigin
:: o
cdtype
::
MExp
o
cdcont
::
DeclCont
o
cddeffreevars
::
Nat
data
DeclCont
o
Source
Constructors
Def
Nat
[
Clause
o] (
Maybe
Nat
) (
Maybe
Nat
)
Datatype
[
ConstRef
o] [
ConstRef
o]
Constructor
Nat
Postulate
type
Clause
o = ([
Pat
o],
MExp
o)
Source
data
Pat
o
Source
Constructors
PatConApp
(
ConstRef
o) [
Pat
o]
PatVar
String
PatExp
type
ConstRef
o =
IORef
(
ConstDef
o)
Source
data
Elr
o
Source
Constructors
Var
Nat
Const
(
ConstRef
o)
data
Sort
Source
Constructors
Set
Nat
UnknownSort
Type
data
Exp
o
Source
Constructors
App
(
Maybe
(
UId
o)) (
OKHandle
(
RefInfo
o)) (
Elr
o) (
MArgList
o)
Lam
FMode
(
Abs
(
MExp
o))
Pi
(
Maybe
(
UId
o))
FMode
Bool
(
MExp
o) (
Abs
(
MExp
o))
Sort
Sort
AbsurdLambda
FMode
type
MExp
o =
MM
(
Exp
o) (
RefInfo
o)
Source
data
ArgList
o
Source
Constructors
ALNil
ALCons
FMode
(
MExp
o) (
MArgList
o)
ALProj
(
MArgList
o) (
MM
(
ConstRef
o) (
RefInfo
o))
FMode
(
MArgList
o)
ALConPar
(
MArgList
o)
type
MArgList
o =
MM
(
ArgList
o) (
RefInfo
o)
Source
data
HNExp
o
Source
Constructors
HNApp
[
Maybe
(
UId
o)] (
Elr
o) (
ICArgList
o)
HNLam
[
Maybe
(
UId
o)]
FMode
(
Abs
(
ICExp
o))
HNPi
[
Maybe
(
UId
o)]
FMode
Bool
(
ICExp
o) (
Abs
(
ICExp
o))
HNSort
Sort
data
HNArgList
o
Source
Constructors
HNALNil
HNALCons
FMode
(
ICExp
o) (
ICArgList
o)
HNALConPar
(
ICArgList
o)
type
ICExp
o =
Clos
(
MExp
o) o
Source
type
CExp
o =
TrBr
(
ICExp
o) o
Source
data
ICArgList
o
Source
Constructors
CALNil
CALConcat
(
Clos
(
MArgList
o) o) (
ICArgList
o)
data
Clos
a o
Source
Constructors
Clos
[
CAction
o] a
data
TrBr
a o
Source
Constructors
TrBr
[
MExp
o] a
data
CAction
o
Source
Constructors
Sub
(
ICExp
o)
Skip
Weak
Nat
type
Ctx
o = [(
MId
,
CExp
o)]
Source
type
EE
=
IO
Source
detecteliminand
:: [
Clause
o] ->
Maybe
Nat
Source
detectsemiflex
::
ConstRef
o -> [
Clause
o] ->
IO
Bool
Source
categorizedecl
::
ConstRef
o ->
IO
()
Source
metaliseokh
::
MExp
o ->
IO
(
MExp
o)
Source
expandExp
::
MExp
o ->
IO
(
MExp
o)
Source
addtrailingargs
::
Clos
(
MArgList
o) o ->
ICArgList
o ->
ICArgList
o
Source
closify
::
MExp
o ->
CExp
o
Source
sub
::
MExp
o ->
CExp
o ->
CExp
o
Source
subi
::
MExp
o ->
ICExp
o ->
ICExp
o
Source
weak
::
Nat
->
CExp
o ->
CExp
o
Source
weaki
::
Nat
->
Clos
a o ->
Clos
a o
Source
weakarglist
::
Nat
->
ICArgList
o ->
ICArgList
o
Source
weakelr
::
Nat
->
Elr
o ->
Elr
o
Source
doclos
:: [
CAction
o] ->
Nat
->
Either
Nat
(
ICExp
o)
Source
Produced by
Haddock
version 2.6.1