summaryrefslogtreecommitdiff
path: root/AvlVerification.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-171-14/+6
| | | | | | | We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: add `find` functionRaito Bezarius2024-04-161-13/+23
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-121-9/+9
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Initial extractionRaito Bezarius2024-03-251-0/+87
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>