| Safe Haskell | None |
|---|
Agda.Syntax.Internal.Generic
- class TermLike a where
- traverseTerm :: (Term -> Term) -> a -> a
- traverseTermM :: (Monad m, Applicative m) => (Term -> m Term) -> a -> m a
- foldTerm :: Monoid m => (Term -> m) -> a -> m
- copyTerm :: (TermLike a, Applicative m, Monad m) => a -> m a
Documentation
Methods
traverseTerm :: (Term -> Term) -> a -> aSource
traverseTermM :: (Monad m, Applicative m) => (Term -> m Term) -> a -> m aSource
Instances
| TermLike LevelAtom | |
| TermLike PlusLevel | |
| TermLike Level | |
| TermLike Type | |
| TermLike Term | |
| TermLike a => TermLike [a] | |
| TermLike a => TermLike (Maybe a) | |
| TermLike a => TermLike (Ptr a) | |
| TermLike a => TermLike (Arg a) | |
| TermLike a => TermLike (Dom a) | |
| TermLike a => TermLike (Abs a) | |
| (TermLike a, TermLike b) => TermLike (a, b) |
copyTerm :: (TermLike a, Applicative m, Monad m) => a -> m aSource
Put it in a monad to make it possible to do strictly.