Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Syntax.Internal.Generic

Synopsis

- 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

class TermLike a where

Methods

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

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

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

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 a

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