From 57b5c3c6d03dbee5a850d2fae4b76817339911a3 Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski Date: Thu, 19 Jun 2025 12:33:25 +0200 Subject: Add instance TestEquality Perm --- src/Data/Array/Nested/Permutation.hs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Data') 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 -- cgit v1.2.3-70-g09d2