From c3b4f56760547940256afea8e692681dbbe21857 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Sun, 9 Mar 2025 22:08:17 +0100
Subject: Clean up code organisation a little

---
 src/CHAD/Types.hs | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/CHAD/Types.hs')

diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs
index fd1b6b1..a8614cf 100644
--- a/src/CHAD/Types.hs
+++ b/src/CHAD/Types.hs
@@ -99,3 +99,10 @@ chcSetAccum :: CHADConfig -> CHADConfig
 chcSetAccum c = c { chcLetArrayAccum = True
                   , chcCaseArrayAccum = True
                   , chcArgArrayAccum = True }
+
+
+------------------------------------ LEMMAS ------------------------------------
+
+indexTupD1Id :: SNat n -> Tup (Replicate n TIx) :~: D1 (Tup (Replicate n TIx))
+indexTupD1Id SZ = Refl
+indexTupD1Id (SS n) | Refl <- indexTupD1Id n = Refl
-- 
cgit v1.2.3-70-g09d2