Agda-2.2.6: A dependently typed functional programming language and proof assistant

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] 

Instances

appView :: Expr -> AppViewSource

headToExpr :: Head -> ExprSource

unAppView :: AppView -> ExprSource