| 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 Source | |
| TermLike Char Source | |
| TermLike Int Source | |
| TermLike Integer Source | |
| TermLike QName Source | |
| TermLike LevelAtom Source | |
| TermLike PlusLevel Source | |
| TermLike Level Source | |
| TermLike Type Source | |
| TermLike Term Source | |
| TermLike a => TermLike [a] Source | |
| TermLike a => TermLike (Maybe a) Source | |
| TermLike a => TermLike (Ptr a) Source | |
| TermLike a => TermLike (Abs a) Source | |
| TermLike a => TermLike (Elim' a) Source | |
| TermLike a => TermLike (Dom a) Source | |
| TermLike a => TermLike (Arg a) Source | |
| (TermLike a, TermLike b) => TermLike (a, b) Source | |
| (TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) Source | |
| (TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) Source |
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.