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

Change review operator again

Browse source
This commit is contained in:
Kiana Sheibani 2023-10-19 14:00:13 -04:00
parent e38d00d4a3
commit ec451f0061
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
(#^) : Review s a -> a -> s (^$) : Review s a -> a -> s
(#^) = review (^$) = 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