From 4b2bfe49196057bfe13ff08a6a909d563dcb69ac Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Wed, 12 Feb 2025 16:23:59 +0300
Subject: [PATCH] [ test ] Adapt tests to `List1` in `SearchBy`

---
 tests/base/deriving_functor/DeriveFunctor.idr  | 2 ++
 tests/base/deriving_functor/expected           | 8 ++++----
 tests/base/deriving_show/DeriveShow.idr        | 2 ++
 tests/base/deriving_traversable/expected       | 2 +-
 tests/idris2/reflection/reflection003/expected | 3 +++
 5 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/tests/base/deriving_functor/DeriveFunctor.idr b/tests/base/deriving_functor/DeriveFunctor.idr
index a0c3b8e25c..06fb2d7543 100644
--- a/tests/base/deriving_functor/DeriveFunctor.idr
+++ b/tests/base/deriving_functor/DeriveFunctor.idr
@@ -8,6 +8,8 @@ import Deriving.Functor
 %logging "derive.functor.clauses" 1
 %logging "derive.functor.assumption" 10
 
+%hide List1
+
 list : Functor List
 list = %runElab derive
 
diff --git a/tests/base/deriving_functor/expected b/tests/base/deriving_functor/expected
index 01e5b22b93..a2ffa2b30f 100644
--- a/tests/base/deriving_functor/expected
+++ b/tests/base/deriving_functor/expected
@@ -79,16 +79,16 @@ LOG derive.functor.clauses:1:
   mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
 LOG derive.functor.clauses:1: 
   mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
-  mapCont f (MkCont x2) = MkCont (\ {arg:6040} => x2 (\ {arg:6042} => {arg:6040} (f {arg:6042})))
+  mapCont f (MkCont x2) = MkCont (\ {arg:6041} => x2 (\ {arg:6043} => {arg:6041} (f {arg:6043})))
 LOG derive.functor.clauses:1: 
   mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
-  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6132} => \ {arg:6139} => x3 {arg:6132} (\ {arg:6141} => {arg:6139} (f {arg:6141})))
+  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6133} => \ {arg:6140} => x3 {arg:6133} (\ {arg:6142} => {arg:6140} (f {arg:6142})))
 LOG derive.functor.clauses:1: 
   mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
-  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6246} => x3 (mapFst (\ t => \ {arg:6248} => t (f {arg:6248})) {arg:6246}))
+  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6247} => x3 (mapFst (\ t => \ {arg:6249} => t (f {arg:6249})) {arg:6247}))
 LOG derive.functor.clauses:1: 
   mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
-  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6370} => x3 (Delay (mapFst (\ t => \ {arg:6373} => t (Delay (f {arg:6373}))) {arg:6370})))
+  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6371} => x3 (Delay (mapFst (\ t => \ {arg:6374} => t (Delay (f {arg:6374}))) {arg:6371})))
 LOG derive.functor.clauses:1: 
   mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
   mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)
diff --git a/tests/base/deriving_show/DeriveShow.idr b/tests/base/deriving_show/DeriveShow.idr
index 8d87731b8d..3c60af7b39 100644
--- a/tests/base/deriving_show/DeriveShow.idr
+++ b/tests/base/deriving_show/DeriveShow.idr
@@ -8,6 +8,8 @@ import Deriving.Show
 %logging "derive.show.clauses" 1
 %logging "derive.show.assumption" 10
 
+%hide List1
+
 namespace Enum
 
   data Enum = A | B | C
diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected
index db9137ffd7..37d9c1b8ab 100644
--- a/tests/base/deriving_traversable/expected
+++ b/tests/base/deriving_traversable/expected
@@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
   traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
   traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
 LOG derive.traversable.clauses:1: 
-  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13929} = eq} a -> f (EqMap key {{conArg:13929} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:16433} = eq} a -> f (EqMap key {{conArg:16433} = eq} b)
   traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
 LOG derive.traversable.clauses:1: 
   traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)
diff --git a/tests/idris2/reflection/reflection003/expected b/tests/idris2/reflection/reflection003/expected
index 1cb9acaa07..14bc1e0f6c 100644
--- a/tests/idris2/reflection/reflection003/expected
+++ b/tests/idris2/reflection/reflection003/expected
@@ -1,4 +1,7 @@
 1/1: Building refprims (refprims.idr)
+LOG 0: Name: Data.List1.(++)
+LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi RigW Explicit (Just xs) (Data.List1.List1 a) (%pi RigW Explicit (Just ys) (Data.List1.List1 a) (Data.List1.List1 a))))
+LOG 0: Pretty Type: (xs : List1 a) -> (ys : List1 a) -> List1 a
 LOG 0: Name: Prelude.Types.List.(++)
 LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi RigW Explicit (Just xs) (Prelude.Basics.List a) (%pi RigW Explicit (Just ys) (Prelude.Basics.List a) (Prelude.Basics.List a))))
 LOG 0: Pretty Type: (xs : List a) -> (ys : List a) -> List a