avl-verification/src, branch main

some isabelle/hol verification

2024-06-29T20:05:40+00:00

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: make `find` extractable

2024-04-18T12:43:41+00:00

I was not borrowing `&self`!

Signed-off-by: Raito Bezarius

feat: add `find` function

2024-04-16T15:46:09+00:00

Signed-off-by: Raito Bezarius

feat: note on extraction for inductive

2024-04-12T18:05:01+00:00

Signed-off-by: Raito Bezarius

feat: commit Rust alternatives

2024-04-12T18:04:37+00:00

Signed-off-by: Raito Bezarius

Initial extraction

2024-03-25T20:09:26+00:00

Signed-off-by: Raito Bezarius

Initial commit

2024-03-25T10:43:20+00:00

Signed-off-by: Raito Bezarius