diff options
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 |