Verify the original overflowing insert implementation
TODO: fill me
TASKS:
-
implement [add_pos] following the original implem -
prove overflowing lemmas -
prove interchange lemmas between go_left t
andt \in full
-
prove interchange -
prove spec of insert_post (Admitted) -
pack insert_pos to build external api
Status: Stuck on the overflown lemma. No longer relevant as super-seeded by the list implementation/.
Edited by Germán Delbianco