toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Change review operator

Browse source
This commit is contained in:
Kiana Sheibani 2023-04-25 13:34:07 -04:00
parent e980b3602d
commit 810404b305
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Control/Lens/Review.idr
View file

@ -66,15 +66,15 @@ public export
review : Review s a -> a -> s review : Review s a -> a -> s
review l = reviews l id review l = reviews l id
infixr 8 >. infixr 8 #^
||| Turn an optic around to inject a focus value into the larger data structure. ||| 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 function takes a `Review`, which can also be a `Prism` or `Iso`.
||| |||
||| This is the operator form of `review`. ||| This is the operator form of `review`.
public export public export
(>.) : a -> Review s a -> s (#^) : Review s a -> a -> s
(>.) x l = review l x (#^) = review
||| Flip a `Prism`, `Iso` or `Review` to form a `Getter` in the other direction. ||| Flip a `Prism`, `Iso` or `Review` to form a `Getter` in the other direction.
public export public export