Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Auto.Syntax
Documentation
data
RefInfo
o
Source
Constructors
RIEnv
[
ConstRef
o]
RIMainInfo
Nat
(
HNExp
o)
forall
a .
RIUnifInfo
(
Metavar
a (
RefInfo
o)) [
CAction
o] (
HNExp
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
data
DeclCont
o
Source
Constructors
Def
Nat
[
Clause
o]
Datatype
[
ConstRef
o]
Constructor
Postulate
type
Clause
o = ([
Pat
o],
MExp
o)
Source
data
Pat
o
Source
Constructors
PatConApp
(
ConstRef
o) [
Pat
o]
PatVar
PatExp
type
ConstRef
o =
IORef
(
ConstDef
o)
Source
data
Elr
o
Source
Constructors
Var
Nat
Const
(
ConstRef
o)
data
Sort
Source
Constructors
SortLevel
Nat
Type
data
Exp
o
Source
Constructors
App
(
Elr
o) (
MArgList
o)
Lam
FMode
(
Abs
(
MExp
o))
Fun
FMode
(
MExp
o) (
MExp
o)
Pi
FMode
Bool
(
MExp
o) (
Abs
(
MExp
o))
Sort
Sort
type
MExp
o =
MM
(
Exp
o) (
RefInfo
o)
Source
data
ArgList
o
Source
Constructors
ALNil
ALCons
FMode
(
MExp
o) (
MArgList
o)
ALConPar
(
MArgList
o)
type
MArgList
o =
MM
(
ArgList
o) (
RefInfo
o)
Source
data
HNExp
o
Source
Constructors
HNApp
(
Elr
o) (
CArgList
o)
HNLam
(
Abs
(
CExp
o))
HNFun
FMode
(
CExp
o) (
CExp
o)
HNPi
FMode
Bool
(
CExp
o) (
Abs
(
CExp
o))
HNSort
Sort
data
HNArgList
o
Source
Constructors
HNALNil
HNALCons
(
CExp
o) (
CArgList
o)
HNALConPar
(
CArgList
o)
type
CExp
o =
Clos
(
MExp
o) o
Source
data
CArgList
o
Source
Constructors
CALNil
CALConcat
(
Clos
(
MArgList
o) o) (
CArgList
o)
data
Clos
a o
Source
Constructors
Clos
[
CAction
o] a
data
CAction
o
Source
Constructors
Sub
(
CExp
o)
Skip
Weak
Nat
type
Ctx
o = [(
MId
,
CExp
o)]
Source
type
EE
=
IO
Source
data
Elrs
o
Source
Constructors
ElrsNil
ElrsCons
(
Elr
o) (
Elrs
o)
ElrsWeak
(
Elrs
o)
Produced by
Haddock
version 2.6.0