summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-125-81/+138
* feat: close the BST proof modulo unbundlingRaito Bezarius2024-04-052-1/+60
* feat: close key theorem for any result on binary search treesRaito Bezarius2024-04-041-25/+26
* feat: lift Rust "totality" to total ordersRaito Bezarius2024-04-041-15/+30
* refactor: define some projectors for ForallNodeRaito Bezarius2024-04-041-0/+6
* refactor: generalize the theory and perform some liftsRaito Bezarius2024-03-286-107/+286
* feat: first property "set of values post = {a} \cup set of values pre"Raito Bezarius2024-03-261-25/+62
* Initial extractionRaito Bezarius2024-03-256-9/+208
* Initial commitRaito Bezarius2024-03-255-0/+122