Agda.Syntax.Concrete.Generic · Agda-2.7.0.1

classclass ExprLike a where

#

Generic traversals for concrete expressions.

Note: does not go into patterns!

Methods

mapExpr :: (Expr -> Expr) -> a -> a
This corresponds to map.
foldExpr :: Monoid m => (Expr -> m) -> a -> m
This corresponds to foldMap.
traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a
This corresponds to mapM.

Instances32ExprLike, …

ExprLike DeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike DoStmtDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike FieldAssignmentDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike LHSDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike LamBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike LamClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike ModuleApplicationDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike ModuleAssignmentDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike BoolDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike ()Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (Arg a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (MaybePlaceholder a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (Ranged a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (WithHiding a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (OpApp a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (RHS' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (TacticAttribute' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (TypedBinding' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (WhereClause' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (List1 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (Maybe a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ExprLike a => ExprLike (Named name a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
(ExprLike a, ExprLike b) => ExprLike (Either a b)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
(ExprLike a, ExprLike b) => ExprLike (a, b)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
(ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
(ExprLike a, ExprLike b, ExprLike c, ExprLike d) => ExprLike (a, b, c, d)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic

classclass FoldDecl a where

#

Methods

foldDecl :: Monoid m => (Declaration -> m) -> a -> m
Collect declarations and subdeclarations, transitively. Prefix-order tree traversal.

Instances5FoldDecl

FoldDecl DeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
FoldDecl a => FoldDecl (WhereClause' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
FoldDecl a => FoldDecl (List1 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
FoldDecl a => FoldDecl (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
FoldDecl a => FoldDecl [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic

classclass TraverseDecl a where

#

Methods

preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> a -> m a
Update declarations and their subdeclarations. Prefix-order traversal: traverses subdeclarations of updated declaration.

Instances5TraverseDecl

TraverseDecl DeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
TraverseDecl a => TraverseDecl (WhereClause' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
TraverseDecl a => TraverseDecl (List1 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
TraverseDecl a => TraverseDecl (List2 a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
TraverseDecl a => TraverseDecl [a]Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic