diff options
| -rw-r--r-- | src/Soat/Data/Product.idr | 15 |
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 |