Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Abstract.Views
Synopsis
data AppView
= Application Head [NamedArg Expr]
| NonApplication Expr
data Head
= HeadVar Name
| HeadDef QName
| HeadCon [QName]
appView :: Expr -> AppView
headToExpr :: Head -> Expr
unAppView :: AppView -> Expr
Documentation
data AppView Source
Constructors
Application Head [NamedArg Expr]
NonApplication ExprTODO: if we allow beta-redexes (which we currently do) there could be one here.
data Head Source
Head of an applicative expression.
Constructors
HeadVar NameA variable.
HeadDef QNameA defined symbol (except constructor).
HeadCon [QName]A constructor which could belong to any of the data types in the list.
appView :: Expr -> AppViewSource
headToExpr :: Head -> ExprSource
unAppView :: AppView -> ExprSource
Produced by Haddock version 2.6.1