diff options
| -rw-r--r-- | src/Soat/Data/Sublist.idr | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr index 98e3c14..ec73723 100644 --- a/src/Soat/Data/Sublist.idr +++ b/src/Soat/Data/Sublist.idr @@ -68,3 +68,9 @@ public export shuffle : is `Sublist` js -> x ^ js -> x ^ is shuffle [] xs = [] shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs + +public export +indexShuffle : (f : is `Sublist` js) -> {0 xs : x ^ js} -> (elem : Elem i is) + -> index (shuffle f xs) elem = index xs (curry f elem) +indexShuffle (mem :: mems) Here = Refl +indexShuffle (mem :: mems) (There elem) = indexShuffle mems elem |