summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-11-24 13:42:32 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-11-24 14:09:24 +0000
commitaa1505c65ef9435d6003da10cf1c5101a5ff70a9 (patch)
treeb1bf21845a39e19b9fcb68fcaaca8e183e2c4f3f /src
parente3747417cdb6e5d24caf4af4cc18d5fd9348a103 (diff)
Iterate over index list for dependent map.
Diffstat (limited to 'src')
-rw-r--r--src/Soat/Data/Product.idr4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index e9c3d17..52f9181 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 [] = []
-map f (x :: xs) = f _ x :: map f xs
+map f {is = []} xs = []
+map f {is = (i :: is)} xs = f _ (head xs) :: map f (tail xs)
public export
(++) : x ^ is -> x ^ js -> x ^ (is ++ js)