From a66e481e8e0f2238dcab6049e234944e9135e49c Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 25 Nov 2022 14:50:07 +0000
Subject: Change recursion structure of map.

---
 src/Soat/Data/Product.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index 52f9181..e9c3d17 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -63,8 +63,8 @@ indexTabulate f (There elem) = indexTabulate (f . There) elem
 
 public export
 map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
-map f {is = []}        xs = []
-map f {is = (i :: is)} xs = f _ (head xs) :: map f (tail xs)
+map f []        = []
+map f (x :: xs) = f _ x :: map f xs
 
 public export
 (++) : x ^ is -> x ^ js -> x ^ (is ++ js)
-- 
cgit v1.2.3