Agda.Syntax.Internal.Generic · Agda-2.8.0.2

classclass TermLike a where

Source#

Generic term traversal.

Note: ignores sorts in terms! (Does not traverse into or collect from them.)

Methods

traverseTermM :: Monad m => (Term -> m Term) -> a -> m a
Generic traversal with post-traversal action. Ignores sorts.
foldTerm :: Monoid m => (Term -> m) -> a -> m
Generic fold, ignoring sorts.

Instances33TermLike, …

TermLike QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike EqualityViewDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike LevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike PlusLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike SortDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike TermDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike TypeDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike CompareAsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
TermLike ConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
TermLike NLPSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
TermLike NLPTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
TermLike NLPatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
TermLike NatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
TermLike IntegerDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike BoolDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike CharDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike IntDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Abs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Blocked a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Dom a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Tele a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Case a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (CompiledClauses' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (WithArity a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (List1 a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
TermLike a => TermLike [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
(TermLike a, TermLike b) => TermLike (a, b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
(TermLike a, TermLike b, TermLike c) => TermLike (a, b, c)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
(TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic