diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-06-19 12:33:25 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-06-19 12:33:25 +0200 |
| commit | 57b5c3c6d03dbee5a850d2fae4b76817339911a3 (patch) | |
| tree | 0160bef1a6227f32546c01bd58fed33d39c087fb /src/Data/Array/Nested | |
| parent | 16ec2aaef12130b2ec6cbd6c83d8688b52fc1577 (diff) | |
Add instance TestEquality Perm
Diffstat (limited to 'src/Data/Array/Nested')
| -rw-r--r-- | src/Data/Array/Nested/Permutation.hs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs index bed2877..1f90dc5 100644 --- a/src/Data/Array/Nested/Permutation.hs +++ b/src/Data/Array/Nested/Permutation.hs @@ -44,6 +44,13 @@ infixr 5 `PCons` deriving instance Show (Perm list) deriving instance Eq (Perm list) +instance TestEquality Perm where + testEquality PNil PNil = Just Refl + testEquality (x `PCons` xs) (y `PCons` ys) + | Just Refl <- testEquality x y + , Just Refl <- testEquality xs ys = Just Refl + testEquality _ _ = Nothing + permRank :: Perm list -> SNat (Rank list) permRank PNil = SNat permRank (_ `PCons` l) | SNat <- permRank l = SNat |