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

Agda.Utils.Generics

Description

Contains some generic utility functions.

Synopsis

- isString :: GenericQ Bool
- everythingBut :: (r -> r -> r) -> GenericQ Bool -> GenericQ r -> GenericQ r
- everywhereBut' :: GenericQ Bool -> GenericT -> GenericT
- everywhereButM' :: Monad m => GenericQ Bool -> GenericM m -> GenericM m

# Documentation

isString :: GenericQ Bool

everythingBut :: (r -> r -> r) -> GenericQ Bool -> GenericQ r -> GenericQ r

everywhereBut' :: GenericQ Bool -> GenericT -> GenericT

Same as everywhereBut except that when the stop condition becomes true, the function is called on the top level term (but not on the children).

everywhereButM' :: Monad m => GenericQ Bool -> GenericM m -> GenericM m