diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 10:33:50 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-04 10:33:50 +0200 |
| commit | a9ac62f66e45e64f83043e0ebda04f0b4b80b913 (patch) | |
| tree | 4de2974a7753e97c1f1040af72f49af904ad9570 /src/Data/Array/Nested/Lemmas.hs | |
| parent | 2095a851760b6bb44ba92b70df1efceff1bad267 (diff) | |
Make ranked and shaped lists newtypes over mixed
Diffstat (limited to 'src/Data/Array/Nested/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Nested/Lemmas.hs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs index fa5611b..e61b148 100644 --- a/src/Data/Array/Nested/Lemmas.hs +++ b/src/Data/Array/Nested/Lemmas.hs @@ -59,7 +59,7 @@ lemReplicatePlusApp _ _ _ = unsafeCoerceRefl lemReplicateEmpty :: proxy n -> Replicate n (Nothing @Nat) :~: '[] -> n :~: 0 lemReplicateEmpty _ Refl = unsafeCoerceRefl --- TODO: make less ad-hoc and rename these three: +-- TODO: make less ad-hoc and rename the following few: lemReplicateCons :: proxy sh -> proxy' n1 -> Nothing : sh :~: Replicate n1 Nothing -> n1 :~: Rank sh + 1 lemReplicateCons _ _ Refl = unsafeCoerceRefl @@ -70,6 +70,10 @@ lemReplicateSucc2 :: forall n1 n proxy. proxy n1 -> n + 1 :~: n1 -> Nothing @Nat : Replicate n Nothing :~: Replicate n1 Nothing lemReplicateSucc2 _ _ = unsafeCoerceRefl +-- TODO: simplify, but GHC doesn't consistently use congruence nor transitivity +lemReplicateHead :: proxy x -> proxy' sh -> proxy'' t -> proxy''' n -> x : sh :~: Replicate n t -> x :~: t +lemReplicateHead _ _ _ _ Refl = unsafeCoerceRefl + lemDropLenApp :: Rank l1 <= Rank l2 => Proxy l1 -> Proxy l2 -> Proxy rest -> DropLen l1 l2 ++ rest :~: DropLen l1 (l2 ++ rest) |