diff options
| -rw-r--r-- | src/Soat/Data/Sublist.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr index 82637ee..98e3c14 100644 --- a/src/Soat/Data/Sublist.idr +++ b/src/Soat/Data/Sublist.idr @@ -24,6 +24,17 @@ uncurry {xs = []} f = [] uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There) public export +uncurryCurry : (f : xs `Sublist` ys) -> uncurry (curry f) = f +uncurryCurry [] = Refl +uncurryCurry (mem :: mems) = cong ((::) mem) (uncurryCurry mems) + +public export +curryUncurry : (0 f : forall x . Elem x xs -> Elem x ys) -> (i : Elem x xs) + -> curry (uncurry f) i = f i +curryUncurry f Here = Refl +curryUncurry f (There elem) = curryUncurry (f . There) elem + +public export Reflexive (List a) Sublist where reflexive = uncurry id |