summaryrefslogtreecommitdiff
path: root/AvlVerification/Specifications.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-171-14/+22
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-121-24/+38
* feat: close the BST proof modulo unbundlingRaito Bezarius2024-04-051-0/+10
* feat: lift Rust "totality" to total ordersRaito Bezarius2024-04-041-15/+30
* refactor: generalize the theory and perform some liftsRaito Bezarius2024-03-281-0/+55