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

	Commit message (Collapse)	Author	Age	Files	Lines
*	some isabelle/hol verificationHEAD main	stuebinm	2024-06-29	1	-0/+17
\| \| \| \| \| \| \| \|	doesn't do much, just proves that the find function won't cause an error. also removes all uses of rust traits, since these are currently broken on the aeneas side.
*	feat: add functional correctness of elements contained in the resulting tree	Raito Bezarius	2024-04-17	1	-0/+5
\| \| \| \| \| \| \|	We revamp the typeclass mechanisms and we add an equality hypothesis now. 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>
*	refactor: generalize the theory and perform some lifts	Raito Bezarius	2024-03-28	1	-0/+11
	Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>