avl-verification/src, branch mainIsabelle fork of https://github.com/RaitoBezarius/avl-verificationhttps://stuebinm.eu/git/avl-verification/atom/src?h=main2024-06-29T20:05:40Zsome isabelle/hol verification2024-06-29T20:05:40Zstuebinm2024-06-29T20:05:40Zurn:sha1:60ec110ebfe85ecbadf2641bdc5315c619766f0e
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` extractable2024-04-18T12:43:41ZRaito Bezarius2024-04-18T12:43:41Zurn:sha1:8ed11ddcc8ccee48300ffee8cf68408a711a51ca
I was not borrowing `&self`!
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: add `find` function2024-04-16T15:46:09ZRaito Bezarius2024-04-16T15:46:09Zurn:sha1:117cd1c0afbc50ffc5a90473cb4c01185188711e
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: note on extraction for inductive2024-04-12T18:05:01ZRaito Bezarius2024-04-12T18:05:01Zurn:sha1:71d7e8af74c052d671968696fdb70cede5b78d8a
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: commit Rust alternatives2024-04-12T18:04:37ZRaito Bezarius2024-04-12T18:04:37Zurn:sha1:33b319d8be7f550fee29e104e263021789a24dab
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Initial extraction2024-03-25T20:09:26ZRaito Bezarius2024-03-25T20:09:26Zurn:sha1:014fc51d291188afd405c33a8281fbb5013ad304
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Initial commit2024-03-25T10:43:20ZRaito Bezarius2024-03-25T10:43:20Zurn:sha1:d6dce7238ad59f67b6b9bad1b3e50984bb69e84e
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>