diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-09-24 20:56:20 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-09-24 20:56:46 +0200 |
| commit | 61f393ff8f4179e1184e715679dcbadf871cde06 (patch) | |
| tree | efaef4c17cdaf4426e5747bb1a66a1e5dfab8684 /src/Data/Array/Nested/Permutation.hs | |
| parent | 2fae6bf7f6704e3dd9a3f73acbdc84331adb1bf0 (diff) | |
WIP
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 03d1640..1eb7be1 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -276,7 +276,6 @@ lemRankDropLen :: forall is sh. (Rank is <= Rank sh) lemRankDropLen ZKX PNil = Refl lemRankDropLen (_ :!% sh) (_ `PCons` is) | Refl <- lemRankDropLen sh is = Refl lemRankDropLen (_ :!% _) PNil = Refl -lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0" lemIndexSucc :: Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l |