Skip to content

Commit

Permalink
update deriving tests
Browse files Browse the repository at this point in the history
  • Loading branch information
dunhamsteve committed Jan 17, 2025
1 parent 7a6356c commit d1801f3
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 7 deletions.
2 changes: 1 addition & 1 deletion tests/base/deriving_foldable/expected
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
foldMapIVect f (MkIVect x2) = foldMap f x2
LOG derive.foldable.clauses:1:
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5702} = eq} a -> b
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5699} = eq} a -> b
foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
LOG derive.foldable.clauses:1:
foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b
Expand Down
10 changes: 5 additions & 5 deletions tests/base/deriving_functor/expected
Original file line number Diff line number Diff line change
Expand Up @@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
mapIVect f (MkIVect x2) = MkIVect (map f x2)
LOG derive.functor.clauses:1:
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5687} = eq} a -> EqMap key {{conArg:5687} = eq} b
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5684} = eq} a -> EqMap key {{conArg:5684} = eq} b
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:6043} => x2 (\ {arg:6045} => {arg:6043} (f {arg:6045})))
mapCont f (MkCont x2) = MkCont (\ {arg:6040} => x2 (\ {arg:6042} => {arg:6040} (f {arg:6042})))
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:6135} => \ {arg:6142} => x3 {arg:6135} (\ {arg:6144} => {arg:6142} (f {arg:6144})))
mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6132} => \ {arg:6139} => x3 {arg:6132} (\ {arg:6141} => {arg:6139} (f {arg:6141})))
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:6249} => x3 (mapFst (\ t => \ {arg:6251} => t (f {arg:6251})) {arg:6249}))
mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6246} => x3 (mapFst (\ t => \ {arg:6248} => t (f {arg:6248})) {arg:6246}))
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:6373} => x3 (Delay (mapFst (\ t => \ {arg:6376} => t (Delay (f {arg:6376}))) {arg:6373})))
mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6370} => x3 (Delay (mapFst (\ t => \ {arg:6373} => t (Delay (f {arg:6373}))) {arg:6370})))
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: 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:13932} = eq} a -> f (EqMap key {{conArg:13932} = eq} b)
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 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

0 comments on commit d1801f3

Please sign in to comment.