From bc1a51ea186bb94e0cf89d08dcfb28d4b3f48d08 Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Wed, 22 Mar 2023 06:19:54 +0100 Subject: [PATCH] [ regression ] revert to previous implementation of Show --- libs/base/Data/List/Quantifiers.idr | 7 ++++++- libs/base/Data/Vect/Quantifiers.idr | 7 ++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/libs/base/Data/List/Quantifiers.idr b/libs/base/Data/List/Quantifiers.idr index f767aecc0..ff8dbaead 100644 --- 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 index b2dc4b4c2..7ee5ca020 100644 --- 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