Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Abstract.Views
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
Constructors
HeadVar Name
HeadDef QName
HeadCon [QName]
appView :: Expr -> AppViewSource
headToExpr :: Head -> ExprSource
unAppView :: AppView -> ExprSource
Produced by Haddock version 2.6.0