[ regression ] revert to previous implementation of Show

idris-lang · May 2, 2023 · bc1a51e · bc1a51e
1 parent 83f5ef2
commit bc1a51e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/libs/base/Data/List/Quantifiers.idr b/libs/base/Data/List/Quantifiers.idr
@@ -122,7 +122,12 @@ namespace All
 
   export
   All (Show . p) xs => Show (All p xs) where
-    show = show . forget . imapProperty (Show . p) show
+    show pxs = "[" ++ show' "" pxs ++ "]"
+      where
+        show' : String -> All (Show . p) xs' => All p xs' -> String
+        show' acc @{[]} [] = acc
+        show' acc @{[_]} [px] = acc ++ show px
+        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
 
   export
   All (Eq . p) xs => Eq (All p xs) where

diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr
@@ -136,7 +136,12 @@ namespace All
 
   export
   All (Show . p) xs => Show (All p xs) where
-    show = show . forget . imapProperty (Show . p) show
+    show pxs = "[" ++ show' "" pxs ++ "]"
+      where
+        show' : String -> All (Show . p) xs' => All p xs' -> String
+        show' acc @{[]} [] = acc
+        show' acc @{[_]} [px] = acc ++ show px
+        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
 
   export
   All (Eq . p) xs => Eq (All p xs) where