aboutsummaryrefslogtreecommitdiff
path: root/TODO
diff options
context:
space:
mode:
Diffstat (limited to 'TODO')
-rw-r--r--TODO1
1 files changed, 1 insertions, 0 deletions
diff --git a/TODO b/TODO
index 45b469d..5ad9eb6 100644
--- a/TODO
+++ b/TODO
@@ -9,6 +9,7 @@ This is a rough outline of upcoming tasks:
[x] This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they
yield the same tree
- Done by showing how indices relate between both trees.
+[x] Prove that if CompleteTree.indexOf returns none, no index exists for which the predicate is true.
[ ] Prove that if CompleteTree.indexOf returns some, CompleteTree.get with that result fulfills the predicate.
[x] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root.
- Done by showing that the new tree contains all elements except the root, and the updated value.