summaryrefslogtreecommitdiff
path: root/AvlVerification/Tree.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* feat: close `find` / `insert` proofsRaito Bezarius2024-04-231-81/+0
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-171-0/+3
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-121-3/+0
* refactor: generalize the theory and perform some liftsRaito Bezarius2024-03-281-0/+81