diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-06-13 13:09:04 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-06-13 13:09:04 +0200 |
| commit | 20173c939486ed6e27b8170e94f666d8ae3df152 (patch) | |
| tree | 36c02005c3f2a20567388c6291e54bc2e4a4e6db /src/Data/Array/Mixed/Permutation.hs | |
| parent | 275847827d7550436eaf8cd10969f1430dae821d (diff) | |
Rename *LengthSNat to *Rank
Diffstat (limited to 'src/Data/Array/Mixed/Permutation.hs')
| -rw-r--r-- | src/Data/Array/Mixed/Permutation.hs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Data/Array/Mixed/Permutation.hs b/src/Data/Array/Mixed/Permutation.hs index ca99b02..331d5e0 100644 --- a/src/Data/Array/Mixed/Permutation.hs +++ b/src/Data/Array/Mixed/Permutation.hs @@ -45,9 +45,9 @@ infixr 5 `PCons` deriving instance Show (Perm list) deriving instance Eq (Perm list) -permLengthSNat :: Perm list -> SNat (Rank list) -permLengthSNat PNil = SNat -permLengthSNat (_ `PCons` l) | SNat <- permLengthSNat l = SNat +permRank :: Perm list -> SNat (Rank list) +permRank PNil = SNat +permRank (_ `PCons` l) | SNat <- permRank l = SNat permFromList :: [Int] -> (forall list. Perm list -> r) -> r permFromList [] k = k PNil @@ -67,7 +67,7 @@ permToList' = map fromIntegral . permToList -- then @Nothing@ is returned. permCheckPermutation :: forall r list. Perm list -> (IsPermutation list => r) -> Maybe r permCheckPermutation = \p k -> - let n = permLengthSNat p + let n = permRank p in case (provePerm1 (Proxy @list) n p, provePerm2 (SNat @0) n p) of (Just Refl, Just Refl) -> Just k _ -> Nothing |