diff options
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 |