summaryrefslogtreecommitdiff
path: root/AvlVerification/BinarySearchTree.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* feat: close `find` / `insert` proofsRaito Bezarius2024-04-231-54/+0
* feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-121-15/+26
* refactor: define some projectors for ForallNodeRaito Bezarius2024-04-041-0/+6
* refactor: generalize the theory and perform some liftsRaito Bezarius2024-03-281-0/+37