Add rtraverse

94acccf2 · locallycompact · c6810158 · 94acccf2
Commit 94acccf2 authored 2 years ago by locallycompact
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

src/Scratch/Record.idr src/Scratch/Record.idr +5 -0

No files found.
--- a/src/Scratch/Record.idr
+++ b/src/Scratch/Record.idr
@@ -31,3 +31,8 @@ export
 rmap : (forall x. f x -> g x) -> Rec f xs -> Rec g xs
 rmap h Nil = Nil
 rmap h (x :: xs) = h x :: rmap h xs
+
+export
+rtraverse : Applicative h => (forall x. f x -> (h . g) x) -> Rec f xs -> h (Rec g xs)
+rtraverse _ Nil = pure Nil
+rtraverse f (x :: xs) = (::) <$> f x <*> rtraverse f xs