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

Safe HaskellNone

Agda.Syntax.Concrete.Generic

Contents

Description

Generic traversal and reduce for concrete syntax, in the style of Generic.

However, here we use the terminology of Traversable.

Synopsis

Documentation

class ExprLike a whereSource

Generic traversals for concrete expressions.

Note: does not go into patterns!

Methods

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

This corresponds to map.

traverseExpr :: (Monad m, Applicative m) => (Expr -> m Expr) -> a -> m aSource

This corresponds to mapM.

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

This is a reduce.

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances