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