diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-14 21:22:20 +0100 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-12-16 09:54:29 +0100 |
| commit | 7e8cb11edf6cb6f46cf92e7dac10e75281992a0a (patch) | |
| tree | 2acab256e512780a95d3daee91a44e6b60642fff /src/Data/Array/Nested/Permutation.hs | |
| parent | b0cc8caff4ccf5df85f3bea743be1f03ddde01c6 (diff) | |
Make ShS a newtype over ShX
TODO: use lemmas in place of the unsafeCoerceRefl
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 6bebcfb..8b46d81 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -215,6 +215,18 @@ ssxIndex p1 p2 i = coerce (listxIndex @(SMayNat ()) p1 p2 i) ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh) ssxPermutePrefix = coerce (listxPermutePrefix @(SMayNat ())) +shxTakeLen :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh) +shxTakeLen = coerce (listxTakeLen @(SMayNat Int)) + +shxDropLen :: Perm is -> IShX sh -> IShX (DropLen is sh) +shxDropLen = coerce (listxDropLen @(SMayNat Int)) + +shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh) +shxPermute = coerce (listxPermute @(SMayNat Int)) + +shxIndex :: Proxy is -> Proxy shT -> SNat i -> IShX sh -> SMayNat Int (Index i sh) +shxIndex p1 p2 i = coerce (listxIndex @(SMayNat Int) p1 p2 i) + shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh) shxPermutePrefix = coerce (listxPermutePrefix @(SMayNat Int)) |