From d2ebddeab7f6f878cbde250765900342e34a6c88 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 19 Oct 2023 16:23:05 -0400
Subject: [PATCH 1/9] Update README

---
 README.md | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index ea93c9d..fea32fe 100644
--- a/README.md
+++ b/README.md
@@ -3,10 +3,14 @@
 This package provides utilities for working with lenses, prisms, traversals,
 and other optics in Idris. This library uses *profunctor optics*.
 
-Eventually, this library will also include elaboration scripts to automatically
-generate lenses for a particular datatype.
+## Comparison to Monocle
 
-## Comparisons
+[Monocle](https://github.com/stefan-hoeck/idris2-monocle) is another Idris 2 library
+for lenses. That library represents lenses using a datatype, which is often less
+efficient at run-time, but results in better error messages and is generally
+simpler to understand.
+
+## Comparisons to Non-Idris Libraries
 
 This library is inspired by the Haskell libraries [lens](https://hackage.haskell.org/package/lens-5.2.2),
 [optics](https://hackage.haskell.org/package/optics) and [fresnel](https://hackage.haskell.org/package/fresnel),
@@ -46,3 +50,7 @@ Or you can install using [pack](https://github.com/stefan-hoeck/idris2-pack):
 pack install lens
 ```
 
+## Thanks
+
+Special thanks to [Stefan Höck](https://github.com/stefan-hoeck) for assistance
+with writing elaboration scripts.

From aabe5a94d093a4ac234ffbc55756d2e82fca278f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 19 Oct 2023 16:23:53 -0400
Subject: [PATCH 2/9] Update version to 0.3.0

---
 lens.ipkg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lens.ipkg b/lens.ipkg
index 386b8b5..d9dc720 100644
--- a/lens.ipkg
+++ b/lens.ipkg
@@ -1,5 +1,5 @@
 package lens
-version = 0.2.0
+version = 0.3.0
 
 brief = "Batteries-included profunctor optics"
 

From 40fd0a3a3b63f5ca1f7b134b5bdfeb25e64fbc47 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 19 Oct 2023 19:57:39 -0400
Subject: [PATCH 3/9] Add lenses for List1

---
 src/Data/List1/Lens.idr | 51 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 src/Data/List1/Lens.idr

diff --git a/src/Data/List1/Lens.idr b/src/Data/List1/Lens.idr
new file mode 100644
index 0000000..70a9d49
--- /dev/null
+++ b/src/Data/List1/Lens.idr
@@ -0,0 +1,51 @@
+module Data.List1.Lens
+
+import Data.List1
+import Data.Profunctor
+import public Control.Lens
+import Data.Tuple.Lens
+
+%default total
+
+||| An isomorphism between a list and its reverse.
+public export
+reversed : Iso (List1 a) (List1 b) (List1 a) (List1 b)
+reversed = iso reverse reverse
+
+
+public export
+cons_ : Iso (List1 a) (List1 b) (a, List a) (b, List b)
+cons_ = iso (\(x:::xs) => (x,xs)) (uncurry (:::))
+
+public export
+head_ : Lens' (List1 a) a
+head_ = cons_ . fst_
+
+public export
+tail_ : Lens' (List1 a) (List a)
+tail_ = cons_ . snd_
+
+public export
+snoc_ : Iso (List1 a) (List1 b) (List a, a) (List b, b)
+snoc_ = iso unsnoc (uncurry lappend . mapSnd singleton)
+
+public export
+init_ : Lens' (List1 a) (List a)
+init_ = snoc_ . fst_
+
+public export
+last_ : Lens' (List1 a) a
+last_ = snoc_ . snd_
+
+
+public export
+Ixed Nat a (List1 a) where
+  ix = element
+
+public export
+Each (List1 a) (List1 b) a b where
+  each = traversed
+
+public export
+Num i => IEach i (List1 a) (List1 b) a b where
+  ieach = itraversed

From 1e6309237b298affc871c5487e893f87c3fb0da9 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 19 Oct 2023 20:22:23 -0400
Subject: [PATCH 4/9] Update lens operators

---
 src/Control/Lens/Lens.idr   | 13 +++++--------
 src/Control/Lens/Setter.idr | 11 ++++++++++-
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
index 648dbad..edd738d 100644
--- a/src/Control/Lens/Lens.idr
+++ b/src/Control/Lens/Lens.idr
@@ -154,7 +154,7 @@ infix 4 <||=; infix 4 <&&=; infix 4 <<+>=
 infix 4 <<%=; infix 4 <<%@=; infix 4 <<.=; infix 4 <<?=; infix 4 <<+=; infix 4 <<*=
 infix 4 <<-=; infix 4 <</=; infix 4 <<||=; infix 4 <<&&=; infix 4 <<<+>=
 
-infixr 2 <<~
+infixr 1 <<<~
 
 
 public export
@@ -403,11 +403,8 @@ public export
 
 
 ||| Run a monadic action and set the focus of an optic in state to the result.
-||| This is different from `(<~)` in that it also passes though the output of
-||| the action.
+||| This is different from `(<~)` and `(<<~)` in that it also passes though
+||| the old value of the optic.
 public export
-(<<~) : MonadState s m => Lens s s a b -> m b -> m b
-(<<~) l x = do
-  v <- x
-  modify $ l @{MkIsLens Function} (const v)
-  pure v
+(<<<~) : MonadState s m => Lens s s a b -> m b -> m a
+(<<<~) l m = l <<.= !m
diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr
index 068e411..cd82eb5 100644
--- a/src/Control/Lens/Setter.idr
+++ b/src/Control/Lens/Setter.idr
@@ -157,6 +157,8 @@ infix 4 %=; infix 4 %@=; infix 4 .=; infix 4 .@=; infix 4 ?=; infix 4 <.=
 infix 4 <?=; infix 4 +=; infix 4 *=; infix 4 -=; infix 4 //=; infix 4 ||=
 infix 4 &&=; infixr 4 <+>=
 
+infix 1 <~
+infixr 1 <<~
 
 ||| Set the focus of an optic to `Just` a value.
 public export
@@ -303,4 +305,11 @@ public export
 ||| variable.
 public export
 (<~) : MonadState s m => Setter s s a b -> m b -> m ()
-(<~) l m = m >>= (l .=)
+(<~) l m = l .= !m
+
+||| Run a monadic action and set the focus of an optic in state to the result.
+||| This is different from `(<~)` in that it also passes though the output of
+||| the action.
+public export
+(<<~) : MonadState s m => Setter s s a b -> m b -> m b
+(<<~) l m = l <.= !m

From a7152cd5823080c35392982abdb4a3bfafe2f81d Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sat, 4 Nov 2023 20:58:54 -0400
Subject: [PATCH 5/9] Combine fixity declarations

Apparently this is something you can do? I wasn't aware of it,
but it's very useful!
---
 src/Control/Lens/Getter.idr  |  3 +--
 src/Control/Lens/Indexed.idr |  4 +---
 src/Control/Lens/Lens.idr    | 17 +++++------------
 src/Control/Lens/Setter.idr  | 12 +++---------
 4 files changed, 10 insertions(+), 26 deletions(-)

diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr
index 6b57f21..185f8db 100644
--- a/src/Control/Lens/Getter.idr
+++ b/src/Control/Lens/Getter.idr
@@ -85,8 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a)
 iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
 
 
-infixl 8 ^.
-infixl 8 ^@.
+infixl 8 ^., ^@.
 
 ||| Access the focus value of an optic, particularly a `Getter`.
 |||
diff --git a/src/Control/Lens/Indexed.idr b/src/Control/Lens/Indexed.idr
index c48214c..f031000 100644
--- a/src/Control/Lens/Indexed.idr
+++ b/src/Control/Lens/Indexed.idr
@@ -93,9 +93,7 @@ icompose @{MkIsIso _} f l l' @{ind} =
   l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
   . lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
 
-infixr 9 <.>
-infixr 9 .>
-infixr 9 <.
+infixr 9 <.>, .>, <.
 
 ||| Compose two indexed optics, returning an optic indexed by a pair of indices.
 |||
diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
index edd738d..c3a6cd2 100644
--- a/src/Control/Lens/Lens.idr
+++ b/src/Control/Lens/Lens.idr
@@ -139,20 +139,13 @@ fusing @{MkIsIso _} l = proextract . l . propure
 -- Operators
 ------------------------------------------------------------------------------
 
-infixr 4 %%~; infix 4 %%=; infix 4 %%@~; infix 4 %%@=
+infixr 4 %%~, %%=, %%@~, %%@=
 
-infixr 4 <%~; infixr 4 <%@~; infixr 4 <+~; infixr 4 <*~; infixr 4 <-~
-infixr 4 </~; infixr 4 <||~; infixr 4 <&&~; infixr 4 <<+>~
+infixr 4 <%~, <%@~, <+~, <*~, <-~, </~, <||~, <&&~, <<+>~
+infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
 
-infixr 4 <<%~; infixr 4 <<%@~; infixr 4 <<.~; infixr 4 <<?~; infixr 4 <<+~
-infixr 4 <<*~; infixr 4 <<-~; infixr 4 <</~; infixr 4 <<||~; infixr 4 <<&&~
-infixr 4 <<<+>~
-
-infix 4 <%=; infix 4 <%@=; infix 4 <+=; infix 4 <*=; infix 4 <-=; infix 4 </=
-infix 4 <||=; infix 4 <&&=; infix 4 <<+>=
-
-infix 4 <<%=; infix 4 <<%@=; infix 4 <<.=; infix 4 <<?=; infix 4 <<+=; infix 4 <<*=
-infix 4 <<-=; infix 4 <</=; infix 4 <<||=; infix 4 <<&&=; infix 4 <<<+>=
+infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
+infix 4 <<%=, <<%@=, <<.=, <<?=, <<+=, <<*=, <<-=, <</=, <<||=, <<&&=, <<<+>=
 
 infixr 1 <<<~
 
diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr
index cd82eb5..a915afd 100644
--- a/src/Control/Lens/Setter.idr
+++ b/src/Control/Lens/Setter.idr
@@ -150,15 +150,9 @@ public export
 -- More operators
 ------------------------------------------------------------------------------
 
-infixr 4 ?~; infixr 4 <.~; infixr 4 <?~; infixr 4 +~; infixr 4 *~; infixr 4 -~
-infixr 4 /~; infixr 4 ||~; infixr 4 &&~; infixr 4 <+>~
-
-infix 4 %=; infix 4 %@=; infix 4 .=; infix 4 .@=; infix 4 ?=; infix 4 <.=
-infix 4 <?=; infix 4 +=; infix 4 *=; infix 4 -=; infix 4 //=; infix 4 ||=
-infix 4 &&=; infixr 4 <+>=
-
-infix 1 <~
-infixr 1 <<~
+infixr 4 ?~, <.~, <?~, +~, *~, -~, /~, ||~, &&~, <+>~
+infix 4 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
+infix 1 <~, <<~
 
 ||| Set the focus of an optic to `Just` a value.
 public export

From 253467ebae6a65eaea9b425e21f93c38d0983c9a Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 29 Jan 2024 21:44:54 -0500
Subject: [PATCH 6/9] Fix definition of elemOf

---
 src/Control/Lens/Fold.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Control/Lens/Fold.idr b/src/Control/Lens/Fold.idr
index e9f9dff..67ff90d 100644
--- a/src/Control/Lens/Fold.idr
+++ b/src/Control/Lens/Fold.idr
@@ -218,7 +218,7 @@ ianyOf = ifoldMapOf @{Any}
 ||| Return `True` if the element occurs in the focuses of the optic.
 public export
 elemOf : Eq a => Fold s a -> a -> s -> Bool
-elemOf l = allOf l . (==)
+elemOf l = anyOf l . (==)
 
 ||| Calculate the number of focuses of the optic.
 public export

From 61acb58a229a833e41e517bc0461993d6a310518 Mon Sep 17 00:00:00 2001
From: Madeleine Sydney <lomiskiam@gmail.com>
Date: Thu, 27 Jun 2024 19:51:31 -0600
Subject: [PATCH 7/9] Derive lenses without prefix_record_projections

---
 src/Derive/Lens.idr | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Derive/Lens.idr b/src/Derive/Lens.idr
index cd2bbd6..250e331 100644
--- a/src/Derive/Lens.idr
+++ b/src/Derive/Lens.idr
@@ -5,6 +5,11 @@ import public Language.Reflection.Util
 
 %default total
 
+toField : Name -> Name
+toField (NS ns nm)      = NS ns (toField nm)
+toField (UN (Basic nm)) = UN (Field nm)
+toField nm              = nm
+
 parameters (o : LensOptions)
   lname : Name -> Name
   lname n = UN $ Basic (o.fieldName $ nameStr n)
@@ -17,7 +22,7 @@ parameters (o : LensOptions)
 
   ldef : BoundArg 0 RegularNamed -> Decl
   ldef (BA x _ _) =
-    let fld := argName x
+    let fld := toField $ argName x
         nme := lname fld
         u   := update [ISetField [nameStr fld] `(y)] `(x)
      in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]

From 60231f4a2bbc830be96da6ab83ef44560db618a1 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sat, 29 Jun 2024 01:42:08 -0400
Subject: [PATCH 8/9] Add export declaration to fixities

---
 src/Control/Lens/Fold.idr    |  8 +-------
 src/Control/Lens/Getter.idr  |  2 +-
 src/Control/Lens/Indexed.idr |  2 +-
 src/Control/Lens/Lens.idr    | 12 ++++++------
 src/Control/Lens/Review.idr  |  2 +-
 src/Control/Lens/Setter.idr  | 14 ++++----------
 src/Control/Zipper.idr       |  2 +-
 src/Data/Maybe/Lens.idr      |  2 +-
 8 files changed, 16 insertions(+), 28 deletions(-)

diff --git a/src/Control/Lens/Fold.idr b/src/Control/Lens/Fold.idr
index 67ff90d..e98c9ac 100644
--- a/src/Control/Lens/Fold.idr
+++ b/src/Control/Lens/Fold.idr
@@ -287,7 +287,7 @@ public export
 preview : Fold s a -> s -> Maybe a
 preview = firstOf
 
-infixl 8 ^?
+export infixl 8 ^?, ^@?, ^., ^@.
 
 ||| Access the first focus value of an optic, returning `Nothing` if there are
 ||| no focuses.
@@ -306,8 +306,6 @@ public export
 ipreview : IndexedFold i s a -> s -> Maybe (i, a)
 ipreview = ifirstOf
 
-infixl 8 ^@?
-
 ||| Access the first focus value and index of an indexed optic, returning Nothing
 ||| if there are no focuses.
 |||
@@ -338,8 +336,6 @@ public export
 toListOf : Fold s a -> s -> List a
 toListOf l = foldrOf l (::) []
 
-infixl 8 ^..
-
 ||| Return a list of all focuses of a fold.
 |||
 ||| This is the operator form of `toListOf`.
@@ -353,8 +349,6 @@ public export
 itoListOf : IndexedFold i s a -> s -> List (i, a)
 itoListOf l = ifoldrOf l ((::) .: (,)) []
 
-infixl 8 ^@..
-
 ||| Return a list of all focuses and indices of an indexed fold.
 |||
 ||| This is the operator form of `itoListOf`.
diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr
index 185f8db..bdaaf04 100644
--- a/src/Control/Lens/Getter.idr
+++ b/src/Control/Lens/Getter.idr
@@ -85,7 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a)
 iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
 
 
-infixl 8 ^., ^@.
+export infixl 8 ^., ^@.
 
 ||| Access the focus value of an optic, particularly a `Getter`.
 |||
diff --git a/src/Control/Lens/Indexed.idr b/src/Control/Lens/Indexed.idr
index f031000..a558a63 100644
--- a/src/Control/Lens/Indexed.idr
+++ b/src/Control/Lens/Indexed.idr
@@ -93,7 +93,7 @@ icompose @{MkIsIso _} f l l' @{ind} =
   l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
   . lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
 
-infixr 9 <.>, .>, <.
+export infixr 9 <.>, .>, <.
 
 ||| Compose two indexed optics, returning an optic indexed by a pair of indices.
 |||
diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
index c3a6cd2..d702d3b 100644
--- a/src/Control/Lens/Lens.idr
+++ b/src/Control/Lens/Lens.idr
@@ -139,15 +139,15 @@ fusing @{MkIsIso _} l = proextract . l . propure
 -- Operators
 ------------------------------------------------------------------------------
 
-infixr 4 %%~, %%=, %%@~, %%@=
+export infixr 4 %%~, %%=, %%@~, %%@=
 
-infixr 4 <%~, <%@~, <+~, <*~, <-~, </~, <||~, <&&~, <<+>~
-infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
+export infixr 4 <%~, <%@~, <+~, <*~, <-~, </~, <||~, <&&~, <<+>~
+export infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
 
-infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
-infix 4 <<%=, <<%@=, <<.=, <<?=, <<+=, <<*=, <<-=, <</=, <<||=, <<&&=, <<<+>=
+export infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
+export infix 4 <<%=, <<%@=, <<.=, <<?=, <<+=, <<*=, <<-=, <</=, <<||=, <<&&=, <<<+>=
 
-infixr 1 <<<~
+export infixr 1 <<<~
 
 
 public export
diff --git a/src/Control/Lens/Review.idr b/src/Control/Lens/Review.idr
index 0f03544..c49e9c0 100644
--- a/src/Control/Lens/Review.idr
+++ b/src/Control/Lens/Review.idr
@@ -66,7 +66,7 @@ public export
 review : Review s a -> a -> s
 review l = reviews l id
 
-infixr 8 ^$
+export infixr 8 ^$
 
 ||| 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`.
diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr
index a915afd..1cc2a54 100644
--- a/src/Control/Lens/Setter.idr
+++ b/src/Control/Lens/Setter.idr
@@ -91,7 +91,7 @@ public export
 over : Setter s t a b -> (a -> b) -> s -> t
 over l = l @{MkIsSetter Function}
 
-infixr 4 %~
+export infixr 4 %~, %@~, .~, .@~
 
 ||| Modify the focus or focuses of an optic.
 |||
@@ -106,8 +106,6 @@ public export
 iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
 iover l = l @{MkIsSetter Function} @{Idxed} . uncurry
 
-infixr 4 %@~
-
 ||| Modify the focus or focuses of an indexed optic, having access to the index.
 |||
 ||| This is the operator form of `iover`.
@@ -121,8 +119,6 @@ public export
 set : Setter s t a b -> b -> s -> t
 set l = over l . const
 
-infixr 4 .~
-
 ||| Set the focus or focuses of an optic to a constant value.
 |||
 ||| This is the operator form of `set`.
@@ -136,8 +132,6 @@ public export
 iset : IndexedSetter i s t a b -> (i -> b) -> s -> t
 iset l = iover l . (const .)
 
-infix 4 .@~
-
 ||| Set the focus or focuses of an indexed optic, having access to the index.
 |||
 ||| This is the operator form of `iset`.
@@ -150,9 +144,9 @@ public export
 -- More operators
 ------------------------------------------------------------------------------
 
-infixr 4 ?~, <.~, <?~, +~, *~, -~, /~, ||~, &&~, <+>~
-infix 4 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
-infix 1 <~, <<~
+export infixr 4 ?~, <.~, <?~, +~, *~, -~, /~, ||~, &&~, <+>~
+export infix 4 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
+export infix 1 <~, <<~
 
 ||| Set the focus of an optic to `Just` a value.
 public export
diff --git a/src/Control/Zipper.idr b/src/Control/Zipper.idr
index d6c450a..d293fb3 100644
--- a/src/Control/Zipper.idr
+++ b/src/Control/Zipper.idr
@@ -27,7 +27,7 @@ fromPointer k x (l, r) = l <>> (k,x) :: r
 ------------------------------------------------------------------------------
 
 
-infix 9 @>
+export infix 9 @>
 
 ||| A simple type that represents a layer of the zipper as it moves downwards.
 |||
diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr
index 9f0eaad..67a754f 100644
--- a/src/Data/Maybe/Lens.idr
+++ b/src/Data/Maybe/Lens.idr
@@ -19,7 +19,7 @@ Just_ = prism Just $ \case
   Nothing => Left Nothing
   Just x => Right x
 
-infixl 9 .?
+export infixl 9 .?
 
 ||| The composition `l .? l'` is equivalent to `l . Just_ . l'`.
 ||| Useful for optics whose focus type is a `Maybe`, such as `at`.

From da8f3a05e60673a0700765bdbfdd33f33cb8fd4f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sat, 29 Jun 2024 01:54:11 -0400
Subject: [PATCH 9/9] Fix typo

---
 src/Control/Lens/At.idr        | 2 +-
 src/Control/Lens/Setter.idr    | 4 ++--
 src/Control/Lens/Traversal.idr | 8 ++++----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Control/Lens/At.idr b/src/Control/Lens/At.idr
index 30e6dc4..3d5bdd6 100644
--- a/src/Control/Lens/At.idr
+++ b/src/Control/Lens/At.idr
@@ -37,7 +37,7 @@ public export
 ||| `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`.
 public export
 interface Ixed i v a => Ixed' i i' v a | a where
-  ||| An lens that infallibly accesses a value at a given index of a container.
+  ||| A lens that infallibly accesses a value at a given index of a container.
   ix' : i' -> Lens' a v
 
 ||| An indexed version of `ix'`.
diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr
index 1cc2a54..10eabbc 100644
--- a/src/Control/Lens/Setter.idr
+++ b/src/Control/Lens/Setter.idr
@@ -237,12 +237,12 @@ public export
 ||| Set within a state monad with pass-through.
 public export
 (<.=) : MonadState s m => Setter s s a b -> b -> m b
-(<.=) l x = (l .= x) >> pure x
+(<.=) l x = (l .= x) $> x
 
 ||| Set to `Just` a value within a state monad with pass-through.
 public export
 (<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
-(<?=) l x = (l ?= x) >> pure x
+(<?=) l x = (l ?= x) $> x
 
 ||| Add a constant value to the focus of an optic within a state monad.
 public export
diff --git a/src/Control/Lens/Traversal.idr b/src/Control/Lens/Traversal.idr
index 2fc57ac..2b25502 100644
--- a/src/Control/Lens/Traversal.idr
+++ b/src/Control/Lens/Traversal.idr
@@ -188,7 +188,7 @@ ifailover l = failover (l @{%search} @{Idxed}) . uncurry
 
 partsOf_update : a -> State (List a) a
 partsOf_update x = get >>= \case
-  x' :: xs' => put xs' >> pure x'
+  x' :: xs' => put xs' $> x'
   []        => pure x
 
 ||| Convert a traversal into a lens over a list of values.
@@ -263,12 +263,12 @@ element : Traversable t => Nat -> Optional' (t a) a
 element = elementOf traversed
 
 
-||| Limit a traversal to its first n focuses.
+||| Limit a traversal to its first `n` focuses.
 public export
 taking : Nat -> Traversal s t a a -> Traversal s t a a
 taking n l = elementsOf l (< n)
 
-||| Remove the first n focuses from a traversal.
+||| Remove the first `n` focuses from a traversal.
 public export
 dropping : Nat -> Traversal s t a a -> Traversal s t a a
-dropping i l = elementsOf l (>= i)
+dropping n l = elementsOf l (>= n)