Change recursion structure of Pointwise.

1 files changed, 7 insertions, 8 deletions

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index e9c3d17..cd69098 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -76,10 +76,9 @@ public export
 namespace Pointwise
   public export
   data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
-    Nil  : Pointwise rel {is = Nil} xs xs
-    (::) : forall b . {0 xs, ys : b ^ (i :: is)} -> {0 rel : (i : a) -> Rel (b i)}
-      -> (r : rel i (head xs) (head ys)) -> (rs : Pointwise rel {is} (tail xs) (tail ys))
-      -> Pointwise rel xs ys
+    Nil  : Pointwise rel [] []
+    (::) : 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
   map : forall b . {0 r, s : (i : a) -> Rel (b i)}
@@ -96,10 +95,10 @@ namespace Pointwise
     (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
 
   public export
-  equalImpliesPwEq : {is : List a} -> {0 xs, ys : b ^ is}
-    -> xs = ys -> Pointwise (\_ => Equal) {is} xs ys
-  equalImpliesPwEq {is = []}        Refl = []
-  equalImpliesPwEq {is = (x :: xs)} eq   = cong head eq :: equalImpliesPwEq (cong tail eq)
+  equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys
+  equalImpliesPwEq {xs = []}        {ys = []}        eq = []
+  equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq =
+    cong head eq :: equalImpliesPwEq (cong tail eq)
 
   -- FIXME: work out how to expose interfaces