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

	Commit message (Collapse)	Author	Files	Lines
2024-04-23	feat: make `find` a better specification	Raito Bezarius	1	-10/+18
	Previously, find := true was matching this spec. It needed to be in PRE/POST style and be an equivalence wrt to the location return value. Alternatively, we import the Order. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
2024-04-23	feat: close `find` / `insert` proofs	Raito Bezarius	1	-13/+11
	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: outline of `find` proof	Raito Bezarius	1	-0/+42
	Signed-off-by: Raito Bezarius <masterancpp@gmail.com>