This commit is contained in:
Kiana Sheibani 2024-06-29 01:54:11 -04:00
parent 60231f4a2b
commit da8f3a05e6
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
3 changed files with 7 additions and 7 deletions

View file

@ -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'`.

View file

@ -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

View file

@ -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)