diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-10-02 14:12:15 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-10-02 14:12:15 +0200 |
| commit | 2018dc3476c1a1b723f8c7106d628bd0da8cb49c (patch) | |
| tree | 12255ef1856abc5a7f618c0190a073a5655319bc /src/Data/Array/Nested/Permutation.hs | |
| parent | ef72e54cf6bcee7124058364fea15b4d1bd62cd7 (diff) | |
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 1a0fd22..045b18f 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -283,6 +283,7 @@ lemRankDropLen (_ :!% sh) (_ `PCons` is) = unsafeCoerceRefl #endif lemRankDropLen (_ :!% _) PNil = Refl +lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0" lemIndexSucc :: Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l |