summaryrefslogtreecommitdiff
path: root/AvlVerification.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* feat: close `find` / `insert` proofsRaito Bezarius2024-04-231-2/+3
* feat: extract `find`Raito Bezarius2024-04-181-2/+28
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-171-14/+6
* feat: add `find` functionRaito Bezarius2024-04-161-13/+23
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-121-9/+9
* Initial extractionRaito Bezarius2024-03-251-0/+87