From 27247861d6d3d3247d1ae8e1704e46db07e48d1f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 20 Apr 2023 19:19:13 -0400
Subject: [PATCH] Fix module list in ipkg

---
 lens.ipkg                   | 10 +++++++++-
 src/Control/Lens/Getter.idr |  6 ++++++
 src/Control/Lens/Lens.idr   |  4 ++--
 src/Data/Maybe/Lens.idr     |  4 ++--
 4 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/lens.ipkg b/lens.ipkg
index 4140b91..3baca06 100644
--- a/lens.ipkg
+++ b/lens.ipkg
@@ -13,10 +13,13 @@ langversion >= 0.6.0
 depends = profunctors >= 1.1.2
 
 modules = Control.Applicative.Backwards,
+          Control.Applicative.Indexing,
+          Control.Lens.At,
           Control.Lens.Equality,
           Control.Lens.Fold,
           Control.Lens.Getter,
           Control.Lens.Iso,
+          Control.Lens.Indexed,
           Control.Lens.Lens,
           Control.Lens.Optic,
           Control.Lens.Optional,
@@ -26,4 +29,9 @@ modules = Control.Applicative.Backwards,
           Control.Lens.Setter,
           Control.Lens.Traversal,
           Control.Lens,
-          Data.Bicontravariant
+          Data.Bicontravariant,
+          Data.Either.Lens,
+          Data.List.Lens,
+          Data.Maybe.Lens,
+          Data.Tuple.Lens,
+          Data.Vect.Lens
diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr
index 54f9f2b..6b57f21 100644
--- a/src/Control/Lens/Getter.idr
+++ b/src/Control/Lens/Getter.idr
@@ -73,10 +73,13 @@ public export
 view : Getter s a -> s -> a
 view l = views l id
 
+||| Access the value and index of an optic and apply a function to them,
+||| returning the result.
 public export
 iviews : IndexedGetter i s a -> (i -> a -> r) -> s -> r
 iviews l = runForget . l @{%search} @{Idxed} . MkForget . uncurry
 
+||| Access the focus value and index of an optic, particularly a `Getter`.
 public export
 iview : IndexedGetter i s a -> s -> (i, a)
 iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
@@ -92,6 +95,9 @@ public export
 (^.) : s -> Getter s a -> a
 (^.) x l = view l x
 
+||| Access the focus value and index of an optic, particularly a `Getter`.
+|||
+||| This is the operator form of `iview`.
 public export
 (^@.) : s -> IndexedGetter i s a -> (i, a)
 (^@.) x l = iview l x
diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
index 8f50305..648dbad 100644
--- a/src/Control/Lens/Lens.idr
+++ b/src/Control/Lens/Lens.idr
@@ -108,8 +108,8 @@ withLens l f = uncurry f (getLens l)
 
 ||| `Void` vacuously "contains" a value of any other type.
 public export
-devoid : IndexedLens i Void Void a b
-devoid @{MkIsLens _} = ilens absurd const
+devoid : IndexedLens i Void t a b
+devoid = ilens absurd absurd
 
 ||| All values contain a unit.
 public export
diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr
index e8c02be..74db5cb 100644
--- a/src/Data/Maybe/Lens.idr
+++ b/src/Data/Maybe/Lens.idr
@@ -9,8 +9,8 @@ import public Control.Lens
 
 ||| A prism of the `Nothing` case of a `Maybe`.
 public export
-Nothing_ : Prism' (Maybe a) ()
-Nothing_ = prism' (const Nothing) (guard . isNothing)
+Nothing_ : Prism (Maybe a) (Maybe b) () ()
+Nothing_ = prism (const Nothing) (maybe (Right ()) (const $ Left Nothing))
 
 ||| A prism of the `Just` case of a `Maybe`.
 public export