Agda.Syntax.Internal.Generic

Documentation

class TermLike a where

Minimal complete definition

traverseTerm, traverseTermM, foldTerm

Methods

traverseTerm :: (Term -> Term) -> a -> a

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

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

Instances

TermLike Bool

Methods

traverseTerm :: (Term -> Term) -> Bool -> Bool

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

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

TermLike Char

Methods

traverseTerm :: (Term -> Term) -> Char -> Char

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

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

TermLike Int

Methods

traverseTerm :: (Term -> Term) -> Int -> Int

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

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

TermLike Integer

Methods

traverseTerm :: (Term -> Term) -> Integer -> Integer

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

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

TermLike QName

Methods

traverseTerm :: (Term -> Term) -> QName -> QName

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

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

TermLike EqualityView

Methods

traverseTerm :: (Term -> Term) -> EqualityView -> EqualityView

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

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

TermLike LevelAtom

Methods

traverseTerm :: (Term -> Term) -> LevelAtom -> LevelAtom

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

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

TermLike PlusLevel

Methods

traverseTerm :: (Term -> Term) -> PlusLevel -> PlusLevel

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

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

TermLike Level

Methods

traverseTerm :: (Term -> Term) -> Level -> Level

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

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

TermLike Type

Methods

traverseTerm :: (Term -> Term) -> Type -> Type

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

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

TermLike Term

Methods

traverseTerm :: (Term -> Term) -> Term -> Term

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

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

TermLike Constraint

Methods

traverseTerm :: (Term -> Term) -> Constraint -> Constraint

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

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

TermLike Nat

Methods

traverseTerm :: (Term -> Term) -> Nat -> Nat

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

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

TermLike a => TermLike [a]

Methods

traverseTerm :: (Term -> Term) -> [a] -> [a]

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

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

TermLike a => TermLike (Maybe a)

Methods

traverseTerm :: (Term -> Term) -> Maybe a -> Maybe a

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

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

TermLike a => TermLike (Ptr a)

Methods

traverseTerm :: (Term -> Term) -> Ptr a -> Ptr a

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

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

TermLike a => TermLike (Dom a)

Methods

traverseTerm :: (Term -> Term) -> Dom a -> Dom a

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

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

TermLike a => TermLike (Arg a)

Methods

traverseTerm :: (Term -> Term) -> Arg a -> Arg a

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

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

TermLike a => TermLike (Blocked a)

Methods

traverseTerm :: (Term -> Term) -> Blocked a -> Blocked a

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

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

TermLike a => TermLike (Abs a)

Methods

traverseTerm :: (Term -> Term) -> Abs a -> Abs a

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

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

TermLike a => TermLike (Elim' a)

Methods

traverseTerm :: (Term -> Term) -> Elim' a -> Elim' a

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

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

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

Methods

traverseTerm :: (Term -> Term) -> (a, b) -> (a, b)

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)

Methods

traverseTerm :: (Term -> Term) -> (a, b, c) -> (a, b, c)

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)

Methods

traverseTerm :: (Term -> Term) -> (a, b, c, d) -> (a, b, c, d)

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

Constants

Functors

Real terms

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

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