Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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 Source

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

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

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 Source

Produced by Haddock version 2.6.0