From 8c529393421843a7ccad041d2f29fa90b46bf6b6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 30 Jun 2023 20:45:33 +0100
Subject: Define zippers and prove no cycles exist.

---
 src/Data/Fin/Occurs.idr | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Data/Fin')

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 74199d3..899e2a1 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -9,6 +9,7 @@ import Data.Maybe.Properties
 predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
 predInjective {n = S n} prf = cong S prf
 
+public export
 indexIsSuc : Fin n -> Exists (\k => n = S k)
 indexIsSuc FZ = Evidence _ Refl
 indexIsSuc (FS x) = Evidence _ Refl
-- 
cgit v1.2.3