From 79726a8a669ff879db4ae14b8e27af357dd7c7b7 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sat, 31 Aug 2024 00:05:44 +0200 Subject: Clean up indexOfAuxAddsCurrentIndex slightly. --- TODO | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'TODO') diff --git a/TODO b/TODO index 5ad9eb6..3108a5d 100644 --- a/TODO +++ b/TODO @@ -10,7 +10,7 @@ This is a rough outline of upcoming tasks: 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 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. [x] Prove that heapPop leaves all values in the tree, except the root. -- cgit v1.2.3