summaryrefslogtreecommitdiff
path: root/AvlVerification/Specifications.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* 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