diff options
Diffstat (limited to 'src/Data/Array/Nested/Internal/Lemmas.hs')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Lemmas.hs | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/src/Data/Array/Nested/Internal/Lemmas.hs b/src/Data/Array/Nested/Internal/Lemmas.hs index 5ce5373..f894f78 100644 --- a/src/Data/Array/Nested/Internal/Lemmas.hs +++ b/src/Data/Array/Nested/Internal/Lemmas.hs @@ -25,30 +25,30 @@ lemMapJustApp :: ShS sh1 -> Proxy sh2 lemMapJustApp ZSS _ = Refl lemMapJustApp (_ :$$ sh) p | Refl <- lemMapJustApp sh p = Refl -lemMapJustTakeLen :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh) -lemMapJustTakeLen PNil _ = Refl -lemMapJustTakeLen (_ `PCons` is) (_ :$$ sh) | Refl <- lemMapJustTakeLen is sh = Refl -lemMapJustTakeLen (_ `PCons` _) ZSS = error "TakeLen of empty" - -lemMapJustDropLen :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh) -lemMapJustDropLen PNil _ = Refl -lemMapJustDropLen (_ `PCons` is) (_ :$$ sh) | Refl <- lemMapJustDropLen is sh = Refl -lemMapJustDropLen (_ `PCons` _) ZSS = error "DropLen of empty" - -lemMapJustIndex :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh) -lemMapJustIndex SZ (_ :$$ _) = Refl -lemMapJustIndex (SS (i :: SNat i')) ((_ :: SNat n) :$$ (sh :: ShS sh')) - | Refl <- lemMapJustIndex i sh +lemTakeLenMapJust :: Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh) +lemTakeLenMapJust PNil _ = Refl +lemTakeLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemTakeLenMapJust is sh = Refl +lemTakeLenMapJust (_ `PCons` _) ZSS = error "TakeLen of empty" + +lemDropLenMapJust :: Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh) +lemDropLenMapJust PNil _ = Refl +lemDropLenMapJust (_ `PCons` is) (_ :$$ sh) | Refl <- lemDropLenMapJust is sh = Refl +lemDropLenMapJust (_ `PCons` _) ZSS = error "DropLen of empty" + +lemIndexMapJust :: SNat i -> ShS sh -> Index i (MapJust sh) :~: Just (Index i sh) +lemIndexMapJust SZ (_ :$$ _) = Refl +lemIndexMapJust (SS (i :: SNat i')) ((_ :: SNat n) :$$ (sh :: ShS sh')) + | Refl <- lemIndexMapJust i sh , Refl <- lemIndexSucc (Proxy @i') (Proxy @(Just n)) (Proxy @(MapJust sh')) , Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh') = Refl -lemMapJustIndex _ ZSS = error "Index of empty" +lemIndexMapJust _ ZSS = error "Index of empty" -lemMapJustPermute :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh) -lemMapJustPermute PNil _ = Refl -lemMapJustPermute (i `PCons` is) sh - | Refl <- lemMapJustPermute is sh - , Refl <- lemMapJustIndex i sh +lemPermuteMapJust :: Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh) +lemPermuteMapJust PNil _ = Refl +lemPermuteMapJust (i `PCons` is) sh + | Refl <- lemPermuteMapJust is sh + , Refl <- lemIndexMapJust i sh = Refl lemKnownMapJust :: forall sh. KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh) |