Agda-2.2.6: A dependently typed functional programming language and proof assistant
Agda.Utils.Generics
Description
Contains some generic utility functions.
Synopsis
isString :: GenericQ BoolSource
everythingBut :: (r -> r -> r) -> GenericQ Bool -> GenericQ r -> GenericQ rSource
everywhereBut' :: GenericQ Bool -> GenericT -> GenericTSource
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 mSource