summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* feat: make `find` extractableRaito Bezarius2024-04-181-1/+1
* chore: nixify the projectRaito Bezarius2024-04-185-0/+89
* feat: factor everything in `OrdSpecRel`Raito Bezarius2024-04-172-6/+2
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-176-86/+95
* feat: add `find` functionRaito Bezarius2024-04-162-13/+36
* feat: init lake lockRaito Bezarius2024-04-121-0/+77
* feat: upgrade to lean v4.7Raito Bezarius2024-04-122-9/+2
* feat: note on extraction for inductiveRaito Bezarius2024-04-121-0/+2
* fixup! feat: cleanup more the gitignoreRaito Bezarius2024-04-121-0/+1
* feat: commit Rust alternativesRaito Bezarius2024-04-122-0/+106
* feat: cleanup more the gitignoreRaito Bezarius2024-04-121-0/+1
* feat: init notesRaito Bezarius2024-04-121-0/+114
* feat: cleanup the MainRaito Bezarius2024-04-121-33/+1
* Merge pull request #2 from RaitoBezarius/refactor-theoryRyan Lahfa2024-04-127-116/+433
|\
| * 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:04:22 +0000