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

	Commit message (Collapse)	Author	Files	Lines
2024-06-29	some isabelle/hol verificationHEAD main	stuebinm	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.
2024-04-17	feat: add functional correctness of elements contained in the resulting tree	Raito Bezarius	1	-0/+5
	We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-12	feat: init notes	Raito Bezarius	1	-0/+114
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-03-28	refactor: generalize the theory and perform some lifts	Raito Bezarius	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>