Agda.Syntax.Internal.Generic

Tree traversal for internal syntax.

Documentation

class TermLike a where

Generic term traversal.

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

Minimal complete definition

Nothing

Methods

traverseTermM :: Monad m => (Term -> m Term) -> a -> m a

Generic traversal with post-traversal action. Ignores sorts.

default traverseTermM :: (Monad m, Traversable f, TermLike b, f b ~ a) => (Term -> m Term) -> a -> m a

foldTerm :: Monoid m => (Term -> m) -> a -> m

Generic fold, ignoring sorts.

default foldTerm :: (Monoid m, Foldable f, TermLike b, f b ~ a) => (Term -> m) -> a -> m

Instances

TermLike QName

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName

foldTerm :: Monoid m => (Term -> m) -> QName -> m

TermLike EqualityView

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView

foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m

TermLike Level

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level

foldTerm :: Monoid m => (Term -> m) -> Level -> m

TermLike PlusLevel

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel

foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m

TermLike Sort

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort

foldTerm :: Monoid m => (Term -> m) -> Sort -> m

TermLike Term

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term

foldTerm :: Monoid m => (Term -> m) -> Term -> m

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type

foldTerm :: Monoid m => (Term -> m) -> Type -> m

TermLike CompareAs

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompareAs -> m CompareAs

foldTerm :: Monoid m => (Term -> m) -> CompareAs -> m

TermLike Constraint

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m

TermLike NLPSort

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> NLPSort -> m NLPSort

foldTerm :: Monoid m => (Term -> m) -> NLPSort -> m

TermLike NLPType

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> NLPType -> m NLPType

foldTerm :: Monoid m => (Term -> m) -> NLPType -> m

TermLike NLPat

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> NLPat -> m NLPat

foldTerm :: Monoid m => (Term -> m) -> NLPat -> m

TermLike Nat

Defined in Agda.TypeChecking.Primitive

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat

foldTerm :: Monoid m => (Term -> m) -> Nat -> m

TermLike Integer

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Integer -> m Integer

foldTerm :: Monoid m => (Term -> m) -> Integer -> m

TermLike Bool

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Bool -> m Bool

foldTerm :: Monoid m => (Term -> m) -> Bool -> m

TermLike Char

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Char -> m Char

foldTerm :: Monoid m => (Term -> m) -> Char -> m

TermLike Int

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Int -> m Int

foldTerm :: Monoid m => (Term -> m) -> Int -> m

TermLike a => TermLike (Arg a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a)

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m

TermLike a => TermLike (WithHiding a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a)

foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m

TermLike a => TermLike (Abs a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a)

foldTerm :: Monoid m => (Term -> m) -> Abs a -> m

TermLike a => TermLike (Blocked a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a)

foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m

TermLike a => TermLike (Dom a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a)

foldTerm :: Monoid m => (Term -> m) -> Dom a -> m

TermLike a => TermLike (Tele a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Tele a -> m (Tele a)

foldTerm :: Monoid m => (Term -> m) -> Tele a -> m

TermLike a => TermLike (Elim' a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a)

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m

TermLike a => TermLike (Case a)

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a)

foldTerm :: Monoid m => (Term -> m) -> Case a -> m

TermLike a => TermLike (CompiledClauses' a)

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a)

foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m

TermLike a => TermLike (WithArity a)

Defined in Agda.TypeChecking.CompiledClause

Methods

traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a)

foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m

TermLike a => TermLike (Maybe a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a)

foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m

TermLike a => TermLike [a]

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> [a] -> m [a]

foldTerm :: Monoid m => (Term -> m) -> [a] -> m

(TermLike a, TermLike b) => TermLike (a, b)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b) -> m (a, b)

foldTerm :: Monoid m => (Term -> m) -> (a, b) -> m

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

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c) -> m (a, b, c)

foldTerm :: Monoid m => (Term -> m) -> (a, b, c) -> m

(TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c, d) -> m (a, b, c, d)

foldTerm :: Monoid m => (Term -> m) -> (a, b, c, d) -> m

copyTerm :: (TermLike a, Monad m) => a -> m a

Put it in a monad to make it possible to do strictly.