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

	Commit message (Collapse)	Author	Files	Lines
2024-04-23	feat: close `find` / `insert` proofs	Raito Bezarius	1	-2/+3
	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>
2024-04-18	feat: extract `find`	Raito Bezarius	1	-2/+28
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-17	feat: add functional correctness of elements contained in the resulting tree	Raito Bezarius	1	-14/+6
	We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-16	feat: add `find` function	Raito Bezarius	1	-13/+23
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-12	feat: upgrade and close all proofs except Preorder on U32	Raito Bezarius	1	-9/+9
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-03-25	Initial extraction	Raito Bezarius	1	-0/+87
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>