summaryrefslogtreecommitdiff
path: root/AvlVerification (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-12feat: upgrade and close all proofs except Preorder on U32Raito Bezarius4-72/+129
2024-04-05feat: close the BST proof modulo unbundlingRaito Bezarius2-1/+60
2024-04-04feat: close key theorem for any result on binary search treesRaito Bezarius1-25/+26
2024-04-04feat: lift Rust "totality" to total ordersRaito Bezarius1-15/+30
2024-04-04refactor: define some projectors for ForallNodeRaito Bezarius1-0/+6
2024-03-28refactor: generalize the theory and perform some liftsRaito Bezarius4-0/+260