Agda.Syntax.Internal.Generic

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 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

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