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

	Commit message (Collapse)	Author	Age	Files	Lines
*	feat: close `find` / `insert` proofs	Raito Bezarius	2024-04-23	1	-173/+0
\| \| \| \| \| \| \| \|	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: factor everything in `OrdSpecRel`	Raito Bezarius	2024-04-17	1	-1/+1
\| \| \| \| \| \|	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	1	-57/+58
\| \| \| \| \| \| \|	We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: upgrade and close all proofs except Preorder on U32	Raito Bezarius	2024-04-12	1	-30/+65
\| \| \| \|	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
*	feat: close the BST proof modulo unbundling	Raito Bezarius	2024-04-05	1	-1/+50
\| \| \| \|	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>
*	refactor: generalize the theory and perform some lifts	Raito Bezarius	2024-03-28	1	-0/+87
	Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>