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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Abstract.Views

Contents

Synopsis

Documentation

data AppView Source

Constructors

Application Expr [NamedArg Expr] 

appView :: Expr -> AppView Source

Gather applications to expose head and spine.

Note: everything is an application, possibly of itself to 0 arguments

unAppView :: AppView -> Expr Source

asView :: Pattern -> ([Name], Pattern) Source

Gather top-level AsPatterns to expose underlying pattern.

isSet :: Expr -> Bool Source

Check whether we are dealing with a universe.

unScope :: Expr -> Expr Source

Remove top ScopedExpr wrappers.

deepUnscope :: ExprLike a => a -> a Source

Remove ScopedExpr wrappers everywhere.

NB: Unless the implementation of ExprLike for clauses has been finished, this does not work for clauses yet.

deepUnscopeDecls :: [Declaration] -> [Declaration] Source

deepUnscopeDecl :: Declaration -> [Declaration] Source

Traversal

class ExprLike a where Source

Apply an expression rewriting to every subexpression, inside-out. See Agda.Syntax.Internal.Generic.

Minimal complete definition

Nothing

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a Source

The first expression is pre-traversal, the second one post-traversal.

foldExpr :: Monoid m => (Expr -> m) -> a -> m Source

traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a Source

mapExpr :: (Expr -> Expr) -> a -> a Source

Instances