| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Internal.Generic
Contents
- 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 -> a Source
traverseTermM :: (Monad m, Applicative m) => (Term -> m Term) -> a -> m a Source
Instances
| TermLike Bool | |
| TermLike Char | |
| TermLike Int | |
| TermLike Integer | |
| TermLike QName | |
| 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 (Abs a) | |
| TermLike a => TermLike (Elim' a) | |
| TermLike a => TermLike (Dom a) | |
| TermLike a => TermLike (Arg a) | |
| (TermLike a, TermLike b) => TermLike (a, b) | |
| (TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) | |
| (TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) |
Constants
Functors
Real terms
copyTerm :: (TermLike a, Applicative m, Monad m) => a -> m a Source
Put it in a monad to make it possible to do strictly.