From dfed64700d3caae5749cc94cfcf8b97a4e27a435 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 25 Nov 2022 15:15:40 +0000
Subject: Generalise bindUnique.

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

(limited to 'src/Soat/Data')

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index cd69098..f92c23c 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -109,6 +109,13 @@ namespace Pointwise
   pwRefl f {xs = []}        = []
   pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
 
+
+  public export
+  pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> Reflexive (x i) (rel i))
+    -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys
+  pwReflexive refl Refl = pwRefl refl
+
   public export
   pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
     -> ((i : a) -> Symmetric (x i) (rel i))
-- 
cgit v1.2.3