Agda.Syntax.Abstract.Views

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