| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

HasRange Head

appView :: Expr -> AppView | Source

headToExpr :: Head -> Expr | Source

unAppView :: AppView -> Expr | Source

Produced by Haddock version 2.4.2