Agda-2.2.8: 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 -> AppView Source

headToExpr :: Head -> Expr Source

unAppView :: AppView -> Expr Source