summaryrefslogtreecommitdiff
path: root/AvlVerification/Tree.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-23feat: close `find` / `insert` proofsRaito Bezarius1-81/+0
2024-04-17feat: add functional correctness of elements contained in the resulting treeRaito Bezarius1-0/+3
2024-04-12feat: upgrade and close all proofs except Preorder on U32Raito Bezarius1-3/+0
2024-03-28refactor: generalize the theory and perform some liftsRaito Bezarius1-0/+81