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

Safe Haskell | None

Agda.Syntax.Abstract.Views

Synopsis

- data AppView = Application Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- isSet :: Expr -> Bool

# Documentation

data AppView

Constructors

Application Expr [NamedArg Expr] |

appView :: Expr -> AppView

unAppView :: AppView -> Expr

isSet :: Expr -> Bool

Check whether we are dealing with a universe.