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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal.Generic

Contents

Synopsis

Documentation

class TermLike a where Source #

Minimal complete definition

traverseTerm, traverseTermM, foldTerm

Methods

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

traverseTermM :: Monad m => (Term -> m Term) -> a -> m a Source #

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

Instances

TermLike Bool Source # 

Methods

traverseTerm :: (Term -> Term) -> Bool -> Bool Source #

traverseTermM :: Monad m => (Term -> m Term) -> Bool -> m Bool Source #

foldTerm :: Monoid m => (Term -> m) -> Bool -> m Source #

TermLike Char Source # 

Methods

traverseTerm :: (Term -> Term) -> Char -> Char Source #

traverseTermM :: Monad m => (Term -> m Term) -> Char -> m Char Source #

foldTerm :: Monoid m => (Term -> m) -> Char -> m Source #

TermLike Int Source # 

Methods

traverseTerm :: (Term -> Term) -> Int -> Int Source #

traverseTermM :: Monad m => (Term -> m Term) -> Int -> m Int Source #

foldTerm :: Monoid m => (Term -> m) -> Int -> m Source #

TermLike Integer Source # 

Methods

traverseTerm :: (Term -> Term) -> Integer -> Integer Source #

traverseTermM :: Monad m => (Term -> m Term) -> Integer -> m Integer Source #

foldTerm :: Monoid m => (Term -> m) -> Integer -> m Source #

TermLike QName Source # 

Methods

traverseTerm :: (Term -> Term) -> QName -> QName Source #

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source #

foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #

TermLike EqualityView Source # 
TermLike LevelAtom Source # 
TermLike PlusLevel Source # 
TermLike Level Source # 

Methods

traverseTerm :: (Term -> Term) -> Level -> Level Source #

traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level Source #

foldTerm :: Monoid m => (Term -> m) -> Level -> m Source #

TermLike Type Source # 

Methods

traverseTerm :: (Term -> Term) -> Type -> Type Source #

traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source #

foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #

TermLike Term Source # 

Methods

traverseTerm :: (Term -> Term) -> Term -> Term Source #

traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term Source #

foldTerm :: Monoid m => (Term -> m) -> Term -> m Source #

TermLike Constraint Source # 
TermLike Nat Source # 

Methods

traverseTerm :: (Term -> Term) -> Nat -> Nat Source #

traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat Source #

foldTerm :: Monoid m => (Term -> m) -> Nat -> m Source #

TermLike a => TermLike [a] Source # 

Methods

traverseTerm :: (Term -> Term) -> [a] -> [a] Source #

traverseTermM :: Monad m => (Term -> m Term) -> [a] -> m [a] Source #

foldTerm :: Monoid m => (Term -> m) -> [a] -> m Source #

TermLike a => TermLike (Maybe a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Maybe a -> Maybe a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a) Source #

foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m Source #

TermLike a => TermLike (Ptr a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Ptr a -> Ptr a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Ptr a -> m (Ptr a) Source #

foldTerm :: Monoid m => (Term -> m) -> Ptr a -> m Source #

TermLike a => TermLike (Dom a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Dom a -> Dom a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) Source #

foldTerm :: Monoid m => (Term -> m) -> Dom a -> m Source #

TermLike a => TermLike (Arg a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Arg a -> Arg a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a) Source #

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m Source #

TermLike a => TermLike (Blocked a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Blocked a -> Blocked a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) Source #

foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m Source #

TermLike a => TermLike (Abs a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Abs a -> Abs a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) Source #

foldTerm :: Monoid m => (Term -> m) -> Abs a -> m Source #

TermLike a => TermLike (Elim' a) Source # 

Methods

traverseTerm :: (Term -> Term) -> Elim' a -> Elim' a Source #

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source #

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #

(TermLike a, TermLike b) => TermLike (a, b) Source # 

Methods

traverseTerm :: (Term -> Term) -> (a, b) -> (a, b) Source #

traverseTermM :: Monad m => (Term -> m Term) -> (a, b) -> m (a, b) Source #

foldTerm :: Monoid m => (Term -> m) -> (a, b) -> m Source #

(TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) Source # 

Methods

traverseTerm :: (Term -> Term) -> (a, b, c) -> (a, b, c) Source #

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c) -> m (a, b, c) Source #

foldTerm :: Monoid m => (Term -> m) -> (a, b, c) -> m Source #

(TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) Source # 

Methods

traverseTerm :: (Term -> Term) -> (a, b, c, d) -> (a, b, c, d) Source #

traverseTermM :: Monad m => (Term -> m Term) -> (a, b, c, d) -> m (a, b, c, d) Source #

foldTerm :: Monoid m => (Term -> m) -> (a, b, c, d) -> m Source #

Constants

Functors

Real terms

copyTerm :: (TermLike a, Monad m) => a -> m a Source #

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