diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:31:29 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:31:29 +0000 |
| commit | fec727c164f9f3967eb543406d082f89fe61c052 (patch) | |
| tree | c81578772c18489208e6c7675ae63187111a5321 | |
| parent | a7d205c7d156c81efb3590f30dce62939a9dd088 (diff) | |
Prove index property of shuffle.
| -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 |