Idris2Doc : Data.Withering

Data.Withering

(source)
A withering is something which can be run on any IndWitherable.

Since IndWitherable has a large family of superclasses, there are
many such things.

The interest in these things is that they are the sorts of things
one wants to do in merging operations.

Definitions

dataWithering : (Type->Type) ->Type->Type->Type->Type
Totality: total
Visibility: public export
Constructor: 
MkWithering : Applicativef=> (IndWitherableit=>ta->f (tb)) ->Witheringfiab
runWither : IndWitherableit=>Witheringfiab->ta->f (tb)
Visibility: export
witherOne : Witheringfiab->i->a->f (Maybeb)
Visibility: export
preserving : Applicativef=>Witheringfiaa
Visibility: export
flushing : Applicativef=>Witheringfiab
Visibility: export
mapping : Applicativef=> (a->b) ->Witheringfiab
Visibility: export
imapping : Applicativef=> (i->a->b) ->Witheringfiab
Visibility: export
mapMaybeing : Applicativef=> (a->Maybeb) ->Witheringfiab
Visibility: export
imapMaybeing : Applicativef=> (i->a->Maybeb) ->Witheringfiab
Visibility: export
traversing : Applicativef=> (a->fb) ->Witheringfiab
Visibility: export
itraversing : Applicativef=> (i->a->fb) ->Witheringfiab
Visibility: export
withering : Applicativef=> (a->f (Maybeb)) ->Witheringfiab
Visibility: export
iwithering : Applicativef=> (i->a->f (Maybeb)) ->Witheringfiab
Visibility: export