summaryrefslogtreecommitdiff
path: root/AvlVerification.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* feat: close `find` / `insert` proofsRaito Bezarius2024-04-231-2/+3
| | | | | | | | After a complete 180 with the Order theory, we close the goals of find and insert and we give an example of U32 order that we will upstream to Aeneas directly. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: extract `find`Raito Bezarius2024-04-181-2/+28
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* 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>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:11:17 +0000