diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2025-08-04 18:05:05 +0200 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2025-08-04 18:05:05 +0200 |
| commit | dc66969bc009714486da40254aa3eff3ea57b035 (patch) | |
| tree | 7a671d0703048f2baa3890bba462d99454fe583b /src/Data/Array/Nested/Permutation.hs | |
| parent | 2fae6bf7f6704e3dd9a3f73acbdc84331adb1bf0 (diff) | |
Failed experiment to add replicate/transpose combinationreptrans-failed
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index 03d1640..c893dac 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -281,3 +281,12 @@ lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0" lemIndexSucc :: Proxy i -> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l lemIndexSucc _ _ _ = unsafeCoerceRefl + + +-- * Replication-transpositions + +data RepTrans f sh sh' where + RTNil :: RepTrans f sh '[] + RTUse :: SNat i -> RepTrans f sh sh' -> RepTrans f sh (Index i sh : sh') + RTRep :: f n -> RepTrans f sh sh' -> RepTrans f sh (n : sh') + |