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

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 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

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.

appView :: Expr -> AppView Source

headToExpr :: Head -> Expr Source

unAppView :: AppView -> Expr Source

Produced by Haddock version 2.6.1