Idris2Doc : Control.Lens.Review

Control.Lens.Review

(source)

Definitions

recordIsReview : (Type->Type->Type) ->Type
Totality: total
Visibility: public export
Constructor: 
MkIsReview : (Bifunctorp, (Costrongp, Choicep)) ->IsReviewp

Projection: 
.runIsReview : IsReviewp-> (Bifunctorp, (Costrongp, Choicep))

Hint: 
IsReviewp=>IsPrismp
.runIsReview : IsReviewp-> (Bifunctorp, (Costrongp, Choicep))
Totality: total
Visibility: public export
runIsReview : IsReviewp-> (Bifunctorp, (Costrongp, Choicep))
Totality: total
Visibility: public export
reviewToPrism : IsReviewp=>IsPrismp
Totality: total
Visibility: export
0Review : Type->Type->Type
  A review is an optic whose only capability is being flipped into a `Getter`
in the other direction.

Any `Prism` or `Iso` can be used as a review.

Totality: total
Visibility: public export
unto : (a->s) ->Reviewsa
  Construct a review from an injection function.
Analogous to `to` for getters.

Totality: total
Visibility: public export
un : Gettersa->Reviewas
  Flip a `Getter` to form a `Review`.

Totality: total
Visibility: public export
reviews : Reviewsa-> (e->a) ->e->s
  Turn an optic around to inject a focus value into the larger data structure
after applying a function to it.
This function takes a `Review`, which can also be a `Prism` or `Iso`.

Totality: total
Visibility: public export
review : Reviewsa->a->s
  Turn an optic around to inject a focus value into the larger data structure.
This function takes a `Review`, which can also be a `Prism` or `Iso`.

Totality: total
Visibility: public export
(^$) : Reviewsa->a->s
  Turn an optic around to inject a focus value into the larger data structure.
This function takes a `Review`, which can also be a `Prism` or `Iso`.

This is the operator form of `review`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 8
re : Reviewsa->Getteras
  Flip a `Prism`, `Iso` or `Review` to form a `Getter` in the other direction.

Totality: total
Visibility: public export