1 files changed, 52 insertions, 20 deletions
diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
index a0ed5df..1fcd667 100644
--- a/src/Data/Fin/Strong.idr
+++ b/src/Data/Fin/Strong.idr
@@ -4,11 +4,29 @@ import Data.Fin
 import Decidable.Equality.Core
 import Syntax.PreorderReasoning
 
+-- Definition ------------------------------------------------------------------
+
 public export
 data SFin : Nat -> Type where
   FZ : SFin (S n)
   FS : SFin (S n) -> SFin (S (S n))
 
+-- Properties
+
+export
+Injective (FS {n}) where
+  injective Refl = Refl
+
+export
+Uninhabited (SFin 0) where uninhabited x impossible
+
+export
+Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+
+-- Conversion ------------------------------------------------------------------
+
+-- Utlities
+
 public export
 0 indexPred : (0 x : Fin n) -> Nat
 indexPred {n = S n} x = n
@@ -37,6 +55,8 @@ strongToFin : SFin n -> Fin n
 strongToFin FZ = FZ
 strongToFin (FS x) = FS (strongToFin x)
 
+-- Properties
+
 export
 finToStrongToFin : (x : Fin n) -> strongToFin (finToStrong x) = x
 finToStrongToFin FZ = Refl
@@ -48,20 +68,6 @@ strongToFinToStrong : (x : SFin n) -> finToStrong (strongToFin x) = x
 strongToFinToStrong FZ = Refl
 strongToFinToStrong (FS x) = cong FS (strongToFinToStrong x)
 
-%inline
-export
-FS' : SFin n -> SFin (S n)
-FS' = finToStrong . FS . strongToFin
-
-export
-Injective (FS {n}) where
-  injective Refl = Refl
-
-export
-Injective (FS' {n}) where
-  injective {x = FZ, y = FZ} prf = Refl
-  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
-
 export
 Injective (strongToFin {n}) where
   injective {x, y} prf = Calc $
@@ -70,11 +76,25 @@ Injective (strongToFin {n}) where
     ~~ finToStrong (strongToFin y) ...(cong finToStrong prf)
     ~~ y                           ...(strongToFinToStrong y)
 
+-- Decidable Equality ----------------------------------------------------------
+
 export
-Uninhabited (SFin 0) where uninhabited x impossible
+DecEq (SFin n) where
+  decEq x y = viaEquivalence
+    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
+    (decEq (strongToFin x) (strongToFin y))
 
+-- Useful Constructor ----------------------------------------------------------
+
+%inline
 export
-Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+FS' : SFin n -> SFin (S n)
+FS' = finToStrong . FS . strongToFin
+
+export
+Injective (FS' {n}) where
+  injective {x = FZ, y = FZ} prf = Refl
+  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
 
 export
 sucNonZero : (x : SFin n) -> Not (FS' x = FZ)
@@ -85,8 +105,20 @@ export
 sucIsFS : (x : SFin (S n)) -> FS' x = FS x
 sucIsFS x = rewrite strongToFinToStrong x in Refl
 
+-- Num Interface ---------------------------------------------------------------
+
+public export
+{n : Nat} -> Num (SFin (S n)) where
+  x + y = finToStrong (strongToFin x + strongToFin y)
+  x * y = finToStrong (strongToFin x * strongToFin y)
+  fromInteger = finToStrong . restrict n
+
+-- Weaken and Shift ------------------------------------------------------------
+
 export
-DecEq (SFin n) where
-  decEq x y = viaEquivalence
-    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
-    (decEq (strongToFin x) (strongToFin y))
+weakenN : (0 k : Nat) -> SFin n -> SFin (n + k)
+weakenN k = finToStrong . weakenN k . strongToFin
+
+export
+shift : (k : Nat) -> SFin n -> SFin (k + n)
+shift k = finToStrong . shift k . strongToFin