summaryrefslogtreecommitdiff
path: root/AvlVerification (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-04-17feat: add functional correctness of elements contained in the resulting treeRaito Bezarius3-71/+83
We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-12feat: upgrade and close all proofs except Preorder on U32Raito Bezarius4-72/+129
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-05feat: close the BST proof modulo unbundlingRaito Bezarius2-1/+60
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-04feat: close key theorem for any result on binary search treesRaito Bezarius1-25/+26
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-04feat: lift Rust "totality" to total ordersRaito Bezarius1-15/+30
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-04refactor: define some projectors for ForallNodeRaito Bezarius1-0/+6
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-03-28refactor: generalize the theory and perform some liftsRaito Bezarius4-0/+260
Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>