Agda.Syntax.Concrete.Generic

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

However, here we use the terminology of Traversable.

Documentation

class ExprLike a where

Generic traversals for concrete expressions.

Note: does not go into patterns!

Minimal complete definition

mapExpr

Methods

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

This corresponds to map.

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

This corresponds to mapM.

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

This is a reduce.

Instances

ExprLike QName

ExprLike Name

ExprLike ModuleApplication

ExprLike Declaration

ExprLike LHS

ExprLike TypedBindings

ExprLike LamBinding

ExprLike Expr

ExprLike a => ExprLike [a]

ExprLike a => ExprLike (Maybe a)

ExprLike a => ExprLike (WhereClause' a)

ExprLike a => ExprLike (RHS' a)

ExprLike a => ExprLike (TypedBinding' a)

ExprLike a => ExprLike (OpApp a)

ExprLike a => ExprLike (Arg a)

(ExprLike a, ExprLike b) => ExprLike (a, b)

ExprLike a => ExprLike (Named name a)

(ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c)

Instances for things that do not contain expressions.

Instances for functors.

Interesting instances