index
:
BinaryHeap
main
A toy project about formal validation of a Heap in Lean4
Andreas Grois
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Continue heapRemoveLastWithIndexOnlyRemovesOneElement.
Andreas Grois
2024-07-28
1
-11
/
+35
*
Continue on heapRemoveLastWithIndexOnlyRemovesOneElement.
Andreas Grois
2024-07-28
1
-22
/
+53
*
Progress?
Andreas Grois
2024-07-27
1
-3
/
+34
*
Continue heapRemoveLastWithIndexOnlyRemovesOneElement
Andreas Grois
2024-07-27
2
-14
/
+109
*
Partial implementation of heapRemoveLastWithIndexOnlyRemovesOneElement
Andreas Grois
2024-07-26
5
-12
/
+79
*
Finish contains_iff_index_exists
Andreas Grois
2024-07-25
2
-10
/
+92
*
Start contains_iff_index_exists implementation. Unfinished.
Andreas Grois
2024-07-24
6
-35
/
+190
*
Fix performance issue in CompleteTree.contains.
Andreas Grois
2024-07-24
1
-6
/
+7
*
Minor: Fix indentation. Sorry.
Andreas Grois
2024-07-24
1
-12
/
+12
*
Add CompleteTree.contains. Decidable Predicate.
Andreas Grois
2024-07-24
1
-0
/
+28
*
Add CompleteTree/AdditionalOperations.lean for non-heap operations.
Andreas Grois
2024-07-23
4
-48
/
+53
*
Split code in multiple source files. Separate proofs and logic.
Andreas Grois
2024-07-23
9
-1148
/
+1220
*
Add GetElem instances.
Andreas Grois
2024-07-22
2
-14
/
+43
*
Initial commit.
Andreas Grois
2024-07-22
11
-0
/
+1543
[prev]