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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Internal.Generic

Contents

Synopsis

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

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.