diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2025-03-09 22:08:17 +0100 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2025-03-09 22:08:17 +0100 |
| commit | c3b4f56760547940256afea8e692681dbbe21857 (patch) | |
| tree | 04e7aeee8ebbd78f937c7b4e34a08bec995beca9 /src/CHAD | |
| parent | da5dbc4ebca51a32b43bec360470c037cab1755f (diff) | |
Clean up code organisation a little
Diffstat (limited to 'src/CHAD')
| -rw-r--r-- | src/CHAD/Types.hs | 7 |
1 files changed, 7 insertions, 0 deletions
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 |