From 5ad68cdb44291318a6bed529fcd1771116d9ca08 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 29 Jan 2025 01:13:43 -0500
Subject: [PATCH] Add unfinS to util

---
 src/Util.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index c2979cb..5a998c4 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -11,6 +11,7 @@ import Data.String
 import Data.List.Lazy
 import Data.List1
 import Data.Vect
+import Data.Fin
 
 %default total
 ```
@@ -137,6 +138,21 @@ Lazily generate all the permutations of a Vect
         (y, z :: ys) :: map (consSnd y) (select (z :: ys))
 ```
 
+## Fin
+
+```idris hide
+namespace Fin
+```
+
+
+```idris
+  ||| Decriment a Fin, wrapping on overflow
+  export
+  unfinS : {n : _} -> Fin n -> Fin n
+  unfinS FZ = last
+  unfinS (FS x) = weaken x
+```
+
 ## Vectors
 
 Define some operations for pairs of numbers, treating them roughly like vectors