diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-09-26 21:09:23 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-09-26 21:22:57 +0200 |
| commit | 24d93b59d75c1ea11f4443965d681236c459b439 (patch) | |
| tree | 85d80732066ce8bc5ac19bb19d343d37086ca181 /src/Data/Array/Nested/Lemmas.hs | |
| parent | 61f393ff8f4179e1184e715679dcbadf871cde06 (diff) | |
Diffstat (limited to 'src/Data/Array/Nested/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Nested/Lemmas.hs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs index e8c3b9e..e089479 100644 --- a/src/Data/Array/Nested/Lemmas.hs +++ b/src/Data/Array/Nested/Lemmas.hs @@ -43,6 +43,8 @@ lemAppLeft _ Refl = Refl lemReplicatePlusApp :: forall n m a. SNat n -> Proxy m -> Proxy a -> Replicate (n + m) a :~: Replicate n a ++ Replicate m a +{- for now, the plugins can't derive a type for this code, see + https://github.com/clash-lang/ghc-typelits-natnormalise/pull/98#issuecomment-3332842214 lemReplicatePlusApp sn _ _ = go sn where go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a @@ -51,6 +53,8 @@ lemReplicatePlusApp sn _ _ = go sn | Refl <- lemReplicateSucc @a n , Refl <- go n = sym (lemReplicateSucc @a (SNat @(n'm1 + m))) +-} +lemReplicatePlusApp _ _ _ = unsafeCoerceRefl lemDropLenApp :: Rank l1 <= Rank l2 => Proxy l1 -> Proxy l2 -> Proxy rest |