Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Syntax.Abstract.Views
Documentation
data
AppView
Source
Constructors
Application
Head
[
NamedArg
Expr
]
NonApplication
Expr
TODO: if we allow beta-redexes (which we currently do) there could be one here.
data
Head
Source
Constructors
HeadVar
Name
HeadDef
QName
HeadCon
[
QName
]
appView
::
Expr
->
AppView
Source
headToExpr
::
Head
->
Expr
Source
unAppView
::
AppView
->
Expr
Source
Produced by
Haddock
version 2.6.0