From e6176d741773e78581043b9a0dec9ce9c63321ec Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Fri, 5 Apr 2024 16:00:32 -0500
Subject: [PATCH 1/2] make Fin publicly exported from FVect module

---
 src/Data/FVect.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/FVect.idr b/src/Data/FVect.idr
index 6cc2778..aafd747 100644
--- a/src/Data/FVect.idr
+++ b/src/Data/FVect.idr
@@ -1,7 +1,7 @@
 module Data.FVect
 
 import Data.Vect
-import Data.Fin
+import public Data.Fin
 import Data.Nat
 import Decidable.Equality
 

From 76b1796f7d294a5fcd345f82b450c60f244f4577 Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Fri, 5 Apr 2024 16:00:57 -0500
Subject: [PATCH 2/2] Add a Capacity module. Bump the version

---
 default.nix                 |  2 +-
 fvect.ipkg                  |  3 ++-
 src/Data/FVect/Capacity.idr | 30 ++++++++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 src/Data/FVect/Capacity.idr

diff --git a/default.nix b/default.nix
index 7b42015..e248118 100644
--- a/default.nix
+++ b/default.nix
@@ -1,7 +1,7 @@
 {buildIdris}: let
   pkg = buildIdris {
     ipkgName = "fvect";
-    version = "0.1.0";
+    version = "0.2.0";
     src = ./.;
     idrisLibraries = [];
   };
diff --git a/fvect.ipkg b/fvect.ipkg
index 35a3a5a..f4412cd 100644
--- a/fvect.ipkg
+++ b/fvect.ipkg
@@ -2,7 +2,8 @@
 package fvect
 sourcedir = "src"
 modules = Data.FVect
-version = 0.1.0
+        , Data.FVect.Capacity
+version = 0.2.0
 authors = "Mathew Polzin"
 license = "MIT"
 sourceloc = "https://github.com/mattpolzin/idris-fvect"
diff --git a/src/Data/FVect/Capacity.idr b/src/Data/FVect/Capacity.idr
new file mode 100644
index 0000000..6eade3b
--- /dev/null
+++ b/src/Data/FVect/Capacity.idr
@@ -0,0 +1,30 @@
+module Data.FVect.Capacity
+
+import Data.FVect
+import Data.Nat
+import Decidable.Equality
+
+finPrf : {n : Nat} -> (x : Fin (S n)) -> Either (finToNat x `LT` n) (finToNat x = n)
+finPrf {n = 0} FZ = Right Refl
+finPrf {n = (S k)} FZ = Left (LTESucc LTEZero)
+finPrf {n = (S k)} (FS x) = bimap LTESucc (\p => cong S p) $ finPrf x
+
+||| A representation of the remaining capacity an FVect has for storage.
+||| A `Full` value has proof that there are `n` values in a vect with capacity `n`.
+||| A `NotFull` value has exactly what you need to `consLT` an additional value onto a vect.
+public export
+data Capacity : Type -> Type where
+  Full : (0 eqPrf : finToNat l = c)
+      -> Capacity (FVect c l e)
+  NotFull : {0 n : Nat}
+         -> {0 len : Fin (S (S n))}
+         -> (0 ltPrf : (finToNat len) `LT` (S n))
+         -> Capacity (FVect (S n) len e)
+
+||| Determine if the given FVect has more capacity for strage or not.
+export
+capacity : {c : Nat} -> {l : Fin (S c)} -> (0 _ : FVect c l e) -> Capacity (FVect c l e)
+capacity {c} _ with (finPrf l)
+  capacity {c}         _ | (Right eq) = Full eq
+  capacity {c = (S k)} _ | (Left lte) = NotFull lte
+