summaryrefslogtreecommitdiff
path: root/AvlVerification.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-23feat: close `find` / `insert` proofsRaito Bezarius1-2/+3
2024-04-18feat: extract `find`Raito Bezarius1-2/+28
2024-04-17feat: add functional correctness of elements contained in the resulting treeRaito Bezarius1-14/+6
2024-04-16feat: add `find` functionRaito Bezarius1-13/+23
2024-04-12feat: upgrade and close all proofs except Preorder on U32Raito Bezarius1-9/+9
2024-03-25Initial extractionRaito Bezarius1-0/+87