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

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

Constructors

Application Head [NamedArg Expr] |
NonApplication Expr | TODO: if we allow beta-redexes (which we currently do) there could be one here.

data Head

`Head` of an applicative expression.

Constructors

HeadVar Name | A variable.
HeadDef QName | A defined symbol (except constructor).
HeadCon [QName] | A constructor which could belong to any of the data types in the list.

Instances

HasRange Head |

appView :: Expr -> AppView

headToExpr :: Head -> Expr

unAppView :: AppView -> Expr