avl-verification - Isabelle fork of https://github.com/RaitoBezarius/avl-verification

	Commit message (Collapse)	Author	Age	Files	Lines
*	feat: outline of `find` proof	Raito Bezarius	2024-04-18	1	-0/+42
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: extract `find`	Raito Bezarius	2024-04-18	1	-2/+28
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: make `find` extractable	Raito Bezarius	2024-04-18	1	-1/+1
\| \| \| \| \| \|	I was not borrowing `&self`! Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	chore: nixify the project	Raito Bezarius	2024-04-18	5	-0/+89
\| \| \| \| \| \|	So that I stop doing `nix run` one-offs! Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: factor everything in `OrdSpecRel`	Raito Bezarius	2024-04-17	2	-6/+2
\| \| \| \| \| \|	Now, we speak only about equivalence. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: add functional correctness of elements contained in the resulting tree	Raito Bezarius	2024-04-17	6	-86/+95
\| \| \| \| \| \| \|	We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: add `find` function	Raito Bezarius	2024-04-16	2	-13/+36
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: init lake lock	Raito Bezarius	2024-04-12	1	-0/+77
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: upgrade to lean v4.7	Raito Bezarius	2024-04-12	2	-9/+2
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: note on extraction for inductive	Raito Bezarius	2024-04-12	1	-0/+2
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	fixup! feat: cleanup more the gitignore	Raito Bezarius	2024-04-12	1	-0/+1
\|
*	feat: commit Rust alternatives	Raito Bezarius	2024-04-12	2	-0/+106
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: cleanup more the gitignore	Raito Bezarius	2024-04-12	1	-0/+1
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: init notes	Raito Bezarius	2024-04-12	1	-0/+114
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: cleanup the Main	Raito Bezarius	2024-04-12	1	-33/+1
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	Merge pull request #2 from RaitoBezarius/refactor-theory	Ryan Lahfa	2024-04-12	7	-116/+433
\|\ \| \| \| \|	refactor: generalize the theory and perform some lifts
\| *	feat: upgrade and close all proofs except Preorder on U32	Raito Bezarius	2024-04-12	5	-81/+138
\| \| \| \| \| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
\| *	feat: close the BST proof modulo unbundling	Raito Bezarius	2024-04-05	2	-1/+60
\| \| \| \| \| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
\| *	feat: close key theorem for any result on binary search trees	Raito Bezarius	2024-04-04	1	-25/+26
\| \| \| \| \| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
\| *	feat: lift Rust "totality" to total orders	Raito Bezarius	2024-04-04	1	-15/+30
\| \| \| \| \| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
\| *	refactor: define some projectors for ForallNode	Raito Bezarius	2024-04-04	1	-0/+6
\| \| \| \| \| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
\| *	refactor: generalize the theory and perform some lifts	Raito Bezarius	2024-03-28	6	-107/+286
\|/ \| \| \| \| \|	Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: first property "set of values post = {a} \cup set of values pre"	Raito Bezarius	2024-03-26	1	-25/+62
\| \| \| \| \| \|	This is a first property which is generic of all BSTs. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	Initial extraction	Raito Bezarius	2024-03-25	6	-9/+208
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	Initial commit	Raito Bezarius	2024-03-25	5	-0/+122
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>