From effca509eb470faa515bdb7e61cdaddc80ed37ff Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 25 Nov 2022 15:28:16 +0000
Subject: Define index on Pointwise.

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

(limited to 'src')

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index 2c5d973..7e0ede0 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -130,6 +130,11 @@ namespace Pointwise
     (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
       -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)
 
+  public export
+  index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
+  index (r :: rs) Here         = r
+  index (r :: rs) (There elem) = index rs elem
+
   public export
   map : forall b . {0 r, s : (i : a) -> Rel (b i)}
     -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
-- 
cgit v1.2.3