BinaryHeap - A toy project about formal validation of a Heap in Lean4

	Commit message (Collapse)	Author	Age	Files	Lines
*	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
\| \| \| \|	This is a preparation step for additional proofs.
*	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