summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* 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-23 01:52:33 +0000