diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-05-31 08:58:35 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-05-31 08:58:49 +0200 |
| commit | eea22885eccfe6f720a24682346159853d386434 (patch) | |
| tree | a2cb82e53168a599cbef05897b529dd76cd94285 /src/Data/Array/Nested/Internal/Shaped.hs | |
| parent | df658b3aaea94e1bae0b332c264c1b3b18fe017b (diff) | |
Rename some commuting lemmas to better names
Diffstat (limited to 'src/Data/Array/Nested/Internal/Shaped.hs')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shaped.hs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Data/Array/Nested/Internal/Shaped.hs b/src/Data/Array/Nested/Internal/Shaped.hs index afa91eb..06c87b0 100644 --- a/src/Data/Array/Nested/Internal/Shaped.hs +++ b/src/Data/Array/Nested/Internal/Shaped.hs @@ -254,9 +254,9 @@ stranspose :: forall is sh a. (IsPermutation is, Rank is <= Rank sh, Elt a) => Perm is -> Shaped sh a -> Shaped (PermutePrefix is sh) a stranspose perm sarr@(Shaped arr) | Refl <- lemRankMapJust (sshape sarr) - , Refl <- lemMapJustTakeLen perm (sshape sarr) - , Refl <- lemMapJustDropLen perm (sshape sarr) - , Refl <- lemMapJustPermute perm (shsTakeLen perm (sshape sarr)) + , Refl <- lemTakeLenMapJust perm (sshape sarr) + , Refl <- lemDropLenMapJust perm (sshape sarr) + , Refl <- lemPermuteMapJust perm (shsTakeLen perm (sshape sarr)) , Refl <- lemMapJustApp (shsPermute perm (shsTakeLen perm (sshape sarr))) (Proxy @(DropLen is sh)) = Shaped (mtranspose perm arr) |