diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-02 11:54:26 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2026-04-02 11:54:26 +0200 |
| commit | 086145dfee33e6e198abc148a6375ce929b2c88f (patch) | |
| tree | 1837166ce6bdcff1554df29bceb34e4ec5796d19 /src/Data/Array/Nested/Permutation.hs | |
| parent | 6e48137f2b7d9613f85599f13dbaa949045f96a6 (diff) | |
Audit remaining uses of KnownNat and SNat patterns
Diffstat (limited to 'src/Data/Array/Nested/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index d2557b6..9254728 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -301,11 +301,11 @@ type family MapSucc is where MapSucc (i : is) = i + 1 : MapSucc is permShift1 :: Perm l -> Perm (0 : MapSucc l) -permShift1 = (SNat @0 `PCons`) . permMapSucc +permShift1 = (SZ `PCons`) . permMapSucc where permMapSucc :: Perm l -> Perm (MapSucc l) permMapSucc PNil = PNil - permMapSucc ((SNat :: SNat i) `PCons` ns) = SNat @(i + 1) `PCons` permMapSucc ns + permMapSucc (sn `PCons` ns) = snatSucc sn `PCons` permMapSucc ns -- | @PermId n@ is the type of the identity permutation of length @n@. type family PermId n where @@ -340,11 +340,11 @@ type family MapPlusN n is where -- TODO: instead of permAppend and permShiftN define permComp :: Perm l1 -> Perm l2 -> Perm (l1 ++ MapPlusN (Rank l1) l2), where all three are valid permutations permShiftN :: forall n l. SNat n -> Perm l -> Perm (PermId n ++ MapPlusN n l) -permShiftN n@SNat = (permId n `permAppend`) . permMapPlusN +permShiftN n = (permId n `permAppend`) . permMapPlusN where permMapPlusN :: Perm l1 -> Perm (MapPlusN n l1) permMapPlusN PNil = PNil - permMapPlusN ((SNat :: SNat i) `PCons` ns) = SNat @(i + n) `PCons` permMapPlusN ns + permMapPlusN (sn `PCons` ns) = snatPlus sn n `PCons` permMapPlusN ns -- * Lemmas |