Skip to content

Commit

Permalink
[ test ] Adapt tests to List1 in SearchBy
Browse files Browse the repository at this point in the history
  • Loading branch information
spcfox committed Feb 12, 2025
1 parent 149012c commit 4b2bfe4
Show file tree
Hide file tree
Showing 5 changed files with 12 additions and 5 deletions.
2 changes: 2 additions & 0 deletions tests/base/deriving_functor/DeriveFunctor.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 4 additions & 4 deletions tests/base/deriving_functor/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 2 additions & 0 deletions tests/base/deriving_show/DeriveShow.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/base/deriving_traversable/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
3 changes: 3 additions & 0 deletions tests/idris2/reflection/reflection003/expected
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit 4b2bfe4

Please sign in to comment.